HomeHome brismu bridi
Theorem List (p. 6 of 11)
< Previous  Next >

Mirrors  >  Metamath Home Page  >  Home Page  >  Theorem List Contents       This page: Page List

Theorem List for brismu bridi - 501-600   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Definitiondf-fatci 501 Definition of {fatci} in terms of {du'u}.
go pa du'u broda kei fatci gi broda
 
Theoremfatcii 502 Inference form of df-fatci 501 (Contributed by la korvo, 10-Mar-2024.)
pa du'u broda kei fatci   =>   ⊢ broda
 
Theoremfatciri 503 Reverse inference form of df-fatci 501 (Contributed by la korvo, 10-Mar-2024.)
broda   =>   ⊢ pa du'u broda kei fatci
 
Theoremfatci-ceihi 504 {cei'i} is absolutely true when abstracted. (Contributed by la korvo, 10-Mar-2024.)
pa du'u cei'i kei fatci
 
2.16.4  {nibli}
 
Syntaxsbnibli 505

selbri nibli
 
Definitiondf-nibli 506 {nibli} internalizes implication.
go pa du'u broda kei nibli pa du'u brode kei gi ganai broda gi brode
 
Theoremniblii 507 Inference form of df-nibli 506 (Contributed by la korvo, 19-Jul-2024.)
pa du'u broda kei nibli pa du'u brode kei   =>   ⊢ ganai broda gi brode
 
Theoremnibliii 508 Inference form of df-nibli 506 (Contributed by la korvo, 19-Jul-2024.)
pa du'u broda kei nibli pa du'u brode kei   &   ⊢ broda   =>   ⊢ brode
 
Theoremnibliri 509 Reverse inference form of df-nibli 506 (Contributed by la korvo, 19-Jul-2024.)
ganai broda gi brode   =>   ⊢ pa du'u broda kei nibli pa du'u brode kei
 
Theoremnibli-refl 510 {nibli} is reflexive. (Contributed by la korvo, 19-Jul-2024.)
pa du'u broda kei nibli pa du'u broda kei
 
2.16.5  {sigda}
 
Syntaxsbsigda 511

selbri sigda
 
Definitiondf-sigda 512 {sigda} internalizes implication.
pa du'u ganai broda gi brode kei sigda pa du'u broda kei pa du'u brode kei
 
2.16.6  {tsida}
 
Syntaxsbtsida 513

selbri tsida
 
Definitiondf-tsida 514 {tsida} internalizes biimplication.
pa du'u go broda gi brode kei tsida pa du'u broda kei pa du'u brode kei
 
2.16.7  {kanxe}
 
Syntaxsbkanxe 515

selbri kanxe
 
Definitiondf-kanxe 516 {kanxe} internalizes conjunction.
pa du'u ge broda gi brode kei kanxe pa du'u broda kei pa du'u brode kei
 
2.16.8  {vlina}
 
Syntaxsbvlina 517

selbri vlina
 
Definitiondf-vlina 518 {vlina} internalizes disjunction.
pa du'u ga broda gi brode kei vlina pa du'u broda kei pa du'u brode kei
 
2.16.9  {nalti}
 
Syntaxsbnalti 519

selbri nalti
 
Definitiondf-nalti-ana 520 {nalti} internalizes negation. This direction adds the {naku} prenex to the second bridi.
pa du'u broda kei nalti pa du'u naku broda kei
 
Definitiondf-nalti-kata 521 {nalti} internalizes negation. This direction adds the {naku} prenex to the first bridi.
pa du'u naku broda kei nalti pa du'u broda kei
 
2.17  Parallel reasoning: {fa'u}
 
2.17.1  {fa'u}
 
Syntaxsfahu 522

sumti ko'a fa'u ko'e
 
Definitiondf-fahu 523 Definition of {fa'u} in terms of {ge}.
go ko'a fa'u ko'e bu'a ko'i fa'u ko'o gi ge ko'a bu'a ko'i gi ko'e bu'a ko'o
 
Theoremfahui 524 Inference form of df-fahu 523 (Contributed by la korvo, 16-Jun-2024.)
ko'a fa'u ko'e bu'a ko'i fa'u ko'o   =>   ⊢ ge ko'a bu'a ko'i gi ko'e bu'a ko'o
 
Theoremfahuil 525 Inference form of df-fahu 523 (Contributed by la korvo, 16-Jun-2024.)
ko'a fa'u ko'e bu'a ko'i fa'u ko'o   =>   ⊢ ko'a bu'a ko'i
 
Theoremfahuir 526 Inference form of df-fahu 523 (Contributed by la korvo, 16-Jun-2024.)
ko'a fa'u ko'e bu'a ko'i fa'u ko'o   =>   ⊢ ko'e bu'a ko'o
 
Theoremfahuri 527 Reverse inference form of df-fahu 523 (Contributed by la korvo, 16-Jun-2024.)
ko'a bu'a ko'i   &   ⊢ ko'e bu'a ko'o   =>   ⊢ ko'a fa'u ko'e bu'a ko'i fa'u ko'o
 
2.18  Deletion: {zi'o}
 
Syntaxsziho 528

sumti zi'o
 
Definitiondf-ziho 529 Definition of {zi'o}. Justified by example 7.4-7 from [CLL] p. 7.
ganai ko'a bo'a gi zi'o bo'a
 
Theoremzihoi 530 Inference form of df-ziho 529 (Contributed by la korvo, 22-Aug-2024.)
ko'a bo'a   =>   ⊢ zi'o bo'a
 
Theoremzihoit 531 Delete the second place of a binary bridi. (Contributed by la korvo, 22-Aug-2024.)
ko'a bu'a ko'e   =>   ⊢ ko'a bu'a zi'o
 
Theoremzihogi 532 First-order generalization of zihoi 530 (Contributed by la korvo, 12-Jul-2025.)
ro da zo'u da bo'a   =>   ⊢ zi'o bo'a
 
2.19  Properties of relations

We investigate several common non-familial properties of relations.

 
2.19.1  Transitivity: {takni}
 
Syntaxsbtakni 533

selbri takni
 
Definitiondf-takni 534* A standard definition of transitive relations.
go ko'a takni ko'e gi ro da poi ke'a cmima ko'e ku'o zo'u ro de poi ke'a cmima ko'e ku'o zo'u ro di poi ke'a cmima ko'e ku'o zo'u ganai ge da ckini de ko'a gi de ckini di ko'a gi da ckini di ko'a
 
Theoremtaknii 535* Inference form of df-takni 534 (Contributed by la korvo, 22-Jun-2024.)
ko'a takni ko'e   =>   ⊢ ro da poi ke'a cmima ko'e ku'o zo'u ro de poi ke'a cmima ko'e ku'o zo'u ro di poi ke'a cmima ko'e ku'o zo'u ganai ge da ckini de ko'a gi de ckini di ko'a gi da ckini di ko'a
 
2.19.2  Symmetry: {kinfi}
 
Syntaxsbkinfi 536

selbri kinfi
 
Definitiondf-kinfi 537* A standard definition of symmetric relations.
go ko'a kinfi ko'e gi ro da poi ke'a cmima ko'e ku'o zo'u ro de poi ke'a cmima ko'e ku'o zo'u ganai da ckini de ko'a gi de ckini da ko'a
 
Theoremkinfiri 538* Reverse inference form of df-kinfi 537 (Contributed by la korvo, 25-Jun-2024.)
ro da poi ke'a cmima ko'e ku'o zo'u ro de poi ke'a cmima ko'e ku'o zo'u ganai da ckini de ko'a gi de ckini da ko'a   =>   ⊢ ko'a kinfi ko'e
 
2.19.3  Reflexivity: {kinra}
 
Syntaxsbkinra 539

selbri kinra
 
Definitiondf-kinra 540 A standard definition of reflexive relations.
go ko'a kinra ko'e gi ro da poi ke'a cmima ko'e ku'o zo'u da ckini da ko'a
 
Theoremkinrari 541 Reverse inference form of df-kinra 540 (Contributed by la korvo, 25-Jun-2024.)
ro da poi ke'a cmima ko'e ku'o zo'u da ckini da ko'a   =>   ⊢ ko'a kinra ko'e
 
Theoremrefl-kinra 542 If a selbri is reflexive over any metasyntactic terbri, then it is reflexive over any domain. (Contributed by la korvo, 13-Aug-2024.)
da bu'a da   =>   ⊢ pa ka ce'u bu'a ce'u kei kinra ko'e
 
Theoremdu-kinra 543 {du} is reflexive over any domain. (Contributed by la korvo, 25-Jun-2024.)
pa ka ce'u du ce'u kei kinra ko'e
 
Theoremgripau-kinra 544 {gripau} is reflexive over any domain. (Contributed by la korvo, 19-Jul-2024.)
pa ka ce'u gripau ce'u kei kinra ko'e
 
2.19.4  Euclidean: {efklipi}, {efklizu}
 
Syntaxsbefklipi 545

selbri efklipi
 
Syntaxsbefklizu 546

selbri efklizu
 
Definitiondf-efklipi 547* A standard definition of right-Euclidean relations.
go ko'a efklipi ko'e gi ro da poi ke'a cmima ko'e ku'o zo'u ro de poi ke'a cmima ko'e ku'o zo'u ro di poi ke'a cmima ko'e ku'o zo'u ganai da ckini de .e di ko'a gi de ckini di ko'a
 
Definitiondf-efklizu 548* A standard definition of left-Euclidean relations.
go ko'a efklizu ko'e gi ro da poi ke'a cmima ko'e ku'o zo'u ro de poi ke'a cmima ko'e ku'o zo'u ro di poi ke'a cmima ko'e ku'o zo'u ganai de .e di ckini da ko'a gi de ckini di ko'a
 
Axiomax-efklipi-sym 549 Every Euclidean reflexive relation is symmetric.
ganai ko'a kinra je efklipi ko'e gi ko'a kinfi ko'e
 
Axiomax-efklizu-sym 550

ganai ko'a kinra je efklizu ko'e gi ko'a kinfi ko'e
 
2.20  Existential quantifiers II: {pa da}
 
Syntaxbpd 551 Syntax for uniqueness quantification.
bridi pa da zo'u broda
 
Definitiondf-pa-da 552 Definition of {pa da} in terms of {su'o da} and {du}.
go pa da zo'u da bo'a gi su'o da zo'u ge da bo'a gi ganai ko'a bo'a gi ko'a du da
 
Theorempa-dai 553 Inference form of pa-da (future) (Contributed by la korvo, 20-Aug-2023.)
pa da zo'u da bo'a   =>   ⊢ su'o da zo'u ge da bo'a gi ganai ko'a bo'a gi ko'a du da
 
Theorempa-dari 554 Reverse inference form of pa-da (future) (Contributed by la korvo, 20-Aug-2023.)
su'o da zo'u ge da bo'a gi ganai ko'a bo'a gi ko'a du da   =>   ⊢ pa da zo'u da bo'a
 
Syntaxbpdp 555 Restriction for first-order uniqueness quantification.
bridi pa da poi ke'a bo'a ku'o zo'u broda
 
Definitiondf-poi-pa 556 Definition of {pa da poi} quantifiers as restricted first-order uniqueness quantifiers.
go pa da poi ke'a bo'a ku'o zo'u broda gi pa da zo'u ganai da bo'a gi broda
 
Theorempoi-pai 557 Inference form of df-poi-pa 556 (Contributed by la korvo, 15-Oct-2024.)
pa da poi ke'a bo'a ku'o zo'u broda   =>   ⊢ pa da zo'u ganai da bo'a gi broda
 
Theorempoi-pari 558 Reverse inference form of df-poi-pa 556 (Contributed by la korvo, 15-Oct-2024.)
pa da zo'u ganai da bo'a gi broda   =>   ⊢ pa da poi ke'a bo'a ku'o zo'u broda
 
2.20.1  Uniqueness: {pombo}
 
Syntaxsbpombo 559

selbri pombo
 
Definitiondf-pombo 560 Definition of {pombo}, by analogy with df-pa-da 552. This is a slightly stronger claim than existential uniqueness; {pa da} asserts that something exists with the given property, but {pombo} goes further and witnesses the thing.
go ko'a pombo ko'e gi ro da zo'u da ckaji ko'e gi'o du ko'a
 
Theorempomboi 561 Inference form of df-pombo 560 (Contributed by la korvo, 8-Jul-2025.)
ko'a pombo ko'e   =>   ⊢ ro da zo'u da ckaji ko'e gi'o du ko'a
 
Theorempombori 562 Reverse inference form of df-pombo 560 (Contributed by la korvo, 8-Jul-2025.)
ro da zo'u da ckaji ko'e gi'o du ko'a   =>   ⊢ ko'a pombo ko'e
 
2.21  Abstract algebra I: magmas, semigroups, monoids
 
2.21.1  Magmas: {klojere}
 
Syntaxsbklojere 563

selbri klojere
 
Definitiondf-klojere 564* Definition of {klojere}. This is our most foundational definition for binary operators for now: a binary operator is a ternary relation closed over a set such that, for every ordered pair of elements in the closure, there is a unique related element. In terms of abstract algebra, our binary operators are magmas.
go pa ka ce'u bu'a ce'u ce'u kei klojere ko'a gi ro da poi ke'a cmima ko'a ku'o zo'u ro de poi ke'a cmima ko'a ku'o zo'u pa di poi ke'a cmima ko'a ku'o zo'u da bu'a de di
 
2.21.2  Semigroups: {kloje}
 
Syntaxsbkloje 565

selbri kloje
 
Definitiondf-kloje 566* Definition of {kloje} in terms of {klojere}: a semigroup is an associative magma.
go pa ka ce'u bu'a ce'u ce'u kei kloje ko'a gi ge pa ka ce'u bu'a ce'u ce'u kei klojere ko'a gi ro da poi ke'a cmima ko'a ku'o zo'u ro de poi ke'a cmima ko'a ku'o zo'u ro di poi ke'a cmima ko'a ku'o zo'u go ge da bu'a de ko'e gi ko'e bu'a di ko'i gi ge de bu'a di ko'e gi di bu'a ko'e ko'i
 
2.21.3  Commutative operators: {cajni}
 
Syntaxsbcajni 567

selbri cajni
 
Definitiondf-cajni 568* Definition of {cajni} in terms of {klojere}.
go pa ka ce'u bu'a ce'u ce'u kei cajni ko'a gi ge pa ka ce'u bu'a ce'u ce'u kei klojere ko'a gi ro da poi ke'a cmima ko'a ku'o zo'u ro de poi ke'a cmima ko'a ku'o zo'u ro di poi ke'a cmima ko'a ku'o zo'u go da bu'a de di gi de bu'a da di
 
2.21.4  Monoids: {sezni}
 
Syntaxsbsezni 569

selbri sezni
 
Definitiondf-sezni 570* Definition of {sezni} in terms of {kloje}: a monoid is a semigroup with an identity element.
go pa ka ce'u bu'a ce'u ce'u kei sezni ko'a gi ge ko'a kloje pa ka ce'u bu'a ce'u ce'u kei gi ro da poi ke'a cmima ko'a ku'o zo'u pa de poi ke'a cmima ko'a ku'o zo'u ge da bu'a de da gi de bu'a da da
 
Theoremsezni-elt 571* The identity element of monoids is unique. (Contributed by la korvo, 16-Oct-2024.)
pa ka ce'u bu'a ce'u ce'u kei sezni ko'a   &   ⊢ da cmima ko'a   =>   ⊢ pa de poi ke'a cmima ko'a ku'o zo'u ge da bu'a de da gi de bu'a da da
 
2.21.5  Groups: {dukni}
 
Syntaxsbdukni 572

selbri dukni
 
PART 3  NUMBERS

We define the standard gadgets of number theory. Our axioms are based on the Robinson axioms for second-order arithmetic over successor, addition, multiplication, and comparison. We apply the standard intuitionistic and Metamath transformations to these axioms in addition to reframing them for a Lojbanic relation-first presentation.

Further directions include proving ax-succ-std 598 by improving the axiom of induction, as well as introducing and proving the other Robinson axioms using induction. At the moment, induction can only handle closed formulae expressible as brirebla ({da bo'a}), which proves to be an obstacle.

 
3.1  Natural numbers

We build the natural numbers first with {li} and {du} to match standard presentations, then again with {kacna'u} to establish properties of the set of natural numbers.

 
3.1.1  Zero: {li no}
 
Syntaxsli 573

sumti li ku'i'a
 
Syntaxp0 574

PA no
 
Theoremsl0 575 Syntax for zero. (Contributed by la korvo, 31-Jul-2024.)
sumti li no
 
3.1.2  Successor I: {bai'ei}, {kacli'e}
 
Syntaxmbaihei 576

PA bai'ei ku'i'a
 
Axiomax-baihei-inj 577* The successor function is injective. A standard axiom of second-order arithmetic.
ganai li bai'ei ku'i'a du li bai'ei ku'i'e gi li ku'i'a du li ku'i'e
 
Theorembaihei-inj 578* Inference form of ax-baihei-inj 577 (Contributed by la korvo, 30-Aug-2024.)
li bai'ei ku'i'a du li bai'ei ku'i'e   =>   ⊢ li ku'i'a du li ku'i'e
 
Syntaxbkaclihe 579

selbri kacli'e
 
Definitiondf-kaclihe 580 Definition of {kacli'e} in terms of {bai'ei}.
go li ku'i'a kacli'e ko'a gi li bai'ei ku'i'a du ko'a
 
Axiomax-succ-zero 581 Zero is not a successor. A standard axiom of second-order arithmetic.
naku ko'a kacli'e li no
 
Theoremsucc-zero-ref 582 Refutation of any claimed predecessor to zero. (Contributed by la korvo, 20-Aug-2023.)
ko'a kacli'e li no   =>   ⊢ gai'o
 
Syntaxp1 583

PA pa
 
Theoremsl1 584 Syntax for one. (Contributed by la korvo, 31-Jul-2024.)
sumti li pa
 
Definitiondf-pa 585 One is the successor of zero.
li pa du li bai'ei no
 
Syntaxp2 586

PA re
 
Theoremsl2 587 Syntax for two. (Contributed by la korvo, 31-Jul-2024.)
sumti li re
 
Definitiondf-re 588 Two is the successor of one.
li re du li bai'ei pa
 
3.1.3  Natural number predicate: {kacna'u}
 
Syntaxbkacnahu 589

selbri kacna'u
 
Axiomax-nat-no 590 Zero is a natural number. A standard axiom of second-order arithmetic.
li no kacna'u
 
Axiomax-nat-pa 591 One is a natural number.
li pa kacna'u
 
3.1.4  Successor II
 
Axiomax-succ-succ 592 Successors of natural numbers are also natural numbers, and each natural number has exactly one successor. This is equivalent to Robinson axiom 2 and, as such, should be provable from ax-baihei-inj 577
ganai ko'a .e ko'e kacli'e ko'i gi ko'a du ko'e
 
Theoremsucc-succi 593 Inference form of ax-succ-succ 592 (Contributed by la korvo, 7-Jul-2024.)
ko'a .e ko'e kacli'e ko'i   =>   ⊢ ko'a du ko'e
 
Axiomax-nat-ind 594* The induction axiom for second-order arithmetic. To accomodate higher-order relations, the selbri parameter is generalized to a brirebla.
ganai ge li no bo'a gi ro da poi ke'a bo'a ku'o zo'u su'o de zo'u ge da kacli'e de gi de bo'a gi ro da poi ke'a kacna'u ku'o zo'u da bo'a
 
Theoremnat-indi 595* Inference form of ax-nat-ind 594 (Contributed by la korvo, 10-Aug-2023.)
ge li no bo'a gi ro da poi ke'a bo'a ku'o zo'u su'o de zo'u ge da kacli'e de gi de bo'a   =>   ⊢ ro da poi ke'a kacna'u ku'o zo'u da bo'a
 
Theoremnat-indii 596* Inference form of ax-nat-ind 594 (Contributed by la korvo, 10-Aug-2023.)
li no bo'a   &   ⊢ ro da poi ke'a bo'a ku'o zo'u su'o de zo'u ge da kacli'e de gi de bo'a   =>   ⊢ ro da poi ke'a kacna'u ku'o zo'u da bo'a
 
Theoremnat-ind-cur 597* Curried form of ax-nat-ind 594 (Contributed by la korvo, 20-Aug-2023.)
ganai li no bo'a gi ganai ro da poi ke'a bo'a ku'o zo'u su'o de zo'u ge da kacli'e de gi de bo'a gi ro da poi ke'a kacna'u ku'o zo'u da bo'a
 
Axiomax-succ-std 598* There are no non-standard natural numbers. This axiom upgrades our arithmetic from BA, "baby arithmetic", to Robinson's Q. This is Robinson axiom 3.
ro da poi ke'a kacna'u ku'o zo'u ga da du li no gi su'o de zo'u de kacli'e da
 
3.1.5  Addition I: {su'i}
 
Syntaxmsuhi 599*

PA su'i ku'i'a ku'i'e
 
Axiomax-plus-zero 600 Addition with zero. A standard axiom of second-order arithmetic. Robinson's fourth axiom.
li su'i ku'i'a no du li ku'i'a
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1048
  Copyright terms: Public domain < Previous  Next >