HomeTheorem List (p. 6 of 11)
Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List
| Home |
brismu
bridi Theorem List (p. 6 of 11) |
< Previous Next >
|
|
Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List | ||
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Definition | df-bridi-q 501 |
|
| ⊢ pa du'u ko'a bu'a ko'e ko'i ko'o ku bridi pa ka ce'u bu'a ce'u ce'u ce'u ku ko'a ce'o ko'e ce'o ko'i ce'o ko'o | ||
| Syntax | sbselbri 502 |
|
| selbri selbri | ||
| Definition | df-selbri 503 |
|
| ⊢ go ko'a selbri ko'e ko'i gi ko'a se bridi ko'e ko'i | ||
| Theorem | selbrii 504 | Inference form of df-selbri 503 (Contributed by la korvo, 15-Jun-2025.) |
⊢ ko'a selbri ko'e
ko'i  ⊢ ko'a se bridi ko'e ko'i | ||
| Theorem | selbriri 505 | Reverse inference form of df-selbri 503 (Contributed by la korvo, 15-Jun-2025.) |
| ⊢ ko'a se bridi ko'e ko'i ⊢ ko'a selbri ko'e
ko'i | ||
| Syntax | sbfatci 506 |
|
| selbri fatci | ||
| Definition | df-fatci 507 | Definition of {fatci} in terms of {du'u}. |
| ⊢ go pa du'u broda ku fatci gi broda | ||
| Theorem | fatcii 508 | Inference form of df-fatci 507 (Contributed by la korvo, 10-Mar-2024.) |
| ⊢ pa
du'u broda ku fatci ⊢ broda | ||
| Theorem | fatciri 509 | Reverse inference form of df-fatci 507 (Contributed by la korvo, 10-Mar-2024.) |
| ⊢ broda ⊢ pa du'u broda
ku fatci | ||
| Theorem | fatci-ceihi 510 | {cei'i} is absolutely true when abstracted. (Contributed by la korvo, 10-Mar-2024.) |
| ⊢ pa du'u cei'i ku fatci | ||
| Syntax | sbnibli 511 |
|
| selbri nibli | ||
| Definition | df-nibli 512 | {nibli} internalizes implication. |
| ⊢ go pa du'u broda ku nibli pa du'u brode ku gi ganai broda gi brode | ||
| Theorem | niblii 513 | Inference form of df-nibli 512 (Contributed by la korvo, 19-Jul-2024.) |
| ⊢ pa
du'u broda ku nibli pa du'u
brode ku ⊢ ganai broda gi brode | ||
| Theorem | nibliii 514 | Inference form of df-nibli 512 (Contributed by la korvo, 19-Jul-2024.) |
⊢ pa
du'u broda ku nibli pa du'u
brode ku  ⊢ broda ⊢ brode | ||
| Theorem | nibliri 515 | Reverse inference form of df-nibli 512 (Contributed by la korvo, 19-Jul-2024.) |
| ⊢ ganai broda gi brode ⊢ pa du'u broda
ku nibli pa
du'u brode
ku | ||
| Theorem | nibli-refl 516 | {nibli} is reflexive. (Contributed by la korvo, 19-Jul-2024.) |
| ⊢ pa du'u broda ku nibli pa du'u broda ku | ||
| Syntax | sbsigda 517 |
|
| selbri sigda | ||
| Definition | df-sigda 518 | {sigda} internalizes implication. |
| ⊢ pa du'u ganai broda gi brode ku sigda pa du'u broda ku pa du'u brode ku | ||
| Syntax | sbtsida 519 |
|
| selbri tsida | ||
| Definition | df-tsida 520 | {tsida} internalizes biimplication. |
| ⊢ pa du'u go broda gi brode ku tsida pa du'u broda ku pa du'u brode ku | ||
| Syntax | sbkanxe 521 |
|
| selbri kanxe | ||
| Definition | df-kanxe 522 | {kanxe} internalizes conjunction. |
| ⊢ pa du'u ge broda gi brode ku kanxe pa du'u broda ku pa du'u brode ku | ||
| Syntax | sbvlina 523 |
|
| selbri vlina | ||
| Definition | df-vlina 524 | {vlina} internalizes disjunction. |
| ⊢ pa du'u ga broda gi brode ku vlina pa du'u broda ku pa du'u brode ku | ||
| Syntax | sbnalti 525 |
|
| selbri nalti | ||
| Definition | df-nalti-ana 526 | {nalti} internalizes negation. This direction adds the {naku} prenex to the second bridi. |
| ⊢ pa du'u broda ku nalti pa du'u naku broda ku | ||
| Definition | df-nalti-kata 527 | {nalti} internalizes negation. This direction adds the {naku} prenex to the first bridi. |
| ⊢ pa du'u naku broda ku nalti pa du'u broda ku | ||
| Syntax | sfahu 528 |
|
| sumti ko'a fa'u ko'e | ||
| Definition | df-fahu 529 | 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 | ||
| Theorem | fahui 530 | Inference form of df-fahu 529 (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 | ||
| Theorem | fahuil 531 | Inference form of df-fahu 529 (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 | ||
| Theorem | fahuir 532 | Inference form of df-fahu 529 (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 | ||
| Theorem | fahuri 533 | Reverse inference form of df-fahu 529 (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 | ||
| Syntax | sziho 534 |
|
| sumti zi'o | ||
| Definition | df-ziho 535 | Definition of {zi'o}. Justified by example 7.4-7 from [CLL] p. 7. |
| ⊢ ganai ko'a bo'a gi zi'o bo'a | ||
| Theorem | zihoi 536 | Inference form of df-ziho 535 (Contributed by la korvo, 22-Aug-2024.) |
| ⊢ ko'a bo'a ⊢ zi'o bo'a | ||
| Theorem | zihoit 537 | 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 | ||
| Theorem | zihogi 538 | First-order generalization of zihoi 536 (Contributed by la korvo, 12-Jul-2025.) |
| ⊢ ro da zo'u da
bo'a ⊢ zi'o bo'a | ||
We investigate several common non-familial properties of relations. | ||
| Syntax | sbtakni 539 |
|
| selbri takni | ||
| Definition | df-takni 540* | 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 | ||
| Theorem | taknii 541* | Inference form of df-takni 540 (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 | ||
| Syntax | sbkinfi 542 |
|
| selbri kinfi | ||
| Definition | df-kinfi 543* | 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 | ||
| Theorem | kinfiri 544* | Reverse inference form of df-kinfi 543 (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 | ||
| Syntax | sbkinra 545 |
|
| selbri kinra | ||
| Definition | df-kinra 546 | 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 | ||
| Theorem | kinrari 547 | Reverse inference form of df-kinra 546 (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 | ||
| Theorem | refl-kinra 548 | 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 ku kinra ko'e | ||
| Theorem | du-kinra 549 | {du} is reflexive over any domain. (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ pa ka ce'u du ce'u ku kinra ko'e | ||
| Theorem | gripau-kinra 550 | {gripau} is reflexive over any domain. (Contributed by la korvo, 19-Jul-2024.) |
| ⊢ pa ka ce'u gripau ce'u ku kinra ko'e | ||
| Syntax | sbefklipi 551 |
|
| selbri efklipi | ||
| Syntax | sbefklizu 552 |
|
| selbri efklizu | ||
| Definition | df-efklipi 553* | 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 | ||
| Definition | df-efklizu 554* | 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 | ||
| Axiom | ax-efklipi-sym 555 | Every Euclidean reflexive relation is symmetric. |
| ⊢ ganai ko'a kinra je efklipi ko'e gi ko'a kinfi ko'e | ||
| Axiom | ax-efklizu-sym 556 |
|
| ⊢ ganai ko'a kinra je efklizu ko'e gi ko'a kinfi ko'e | ||
| Syntax | bpd 557 | Syntax for uniqueness quantification. |
| bridi pa da zo'u broda | ||
| Definition | df-pa-da 558 | 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 | ||
| Theorem | pa-dai 559 | 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 | ||
| Theorem | pa-dari 560 | 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 | ||
| Syntax | bpdp 561 | Restriction for first-order uniqueness quantification. |
| bridi pa da poi ke'a bo'a ku'o zo'u broda | ||
| Definition | df-poi-pa 562 | 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 | ||
| Theorem | poi-pai 563 | Inference form of df-poi-pa 562 (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 | ||
| Theorem | poi-pari 564 | Reverse inference form of df-poi-pa 562 (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 | ||
| Syntax | sbpombo 565 |
|
| selbri pombo | ||
| Definition | df-pombo 566 | Definition of {pombo}, by analogy with df-pa-da 558. 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 | ||
| Theorem | pomboi 567 | Inference form of df-pombo 566 (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 | ||
| Theorem | pombori 568 | Reverse inference form of df-pombo 566 (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 | ||
| Syntax | sbklojere 569 |
|
| selbri klojere | ||
| Definition | df-klojere 570* | 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 ku 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 | ||
| Syntax | sbkloje 571 |
|
| selbri kloje | ||
| Definition | df-kloje 572* | Definition of {kloje} in terms of {klojere}: a semigroup is an associative magma. |
| ⊢ go pa ka ce'u bu'a ce'u ce'u ku kloje ko'a gi ge pa ka ce'u bu'a ce'u ce'u ku 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 | ||
| Syntax | sbcajni 573 |
|
| selbri cajni | ||
| Definition | df-cajni 574* | Definition of {cajni} in terms of {klojere}. |
| ⊢ go pa ka ce'u bu'a ce'u ce'u ku cajni ko'a gi ge pa ka ce'u bu'a ce'u ce'u ku 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 | ||
| Syntax | sbsezni 575 |
|
| selbri sezni | ||
| Definition | df-sezni 576* | 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 ku sezni ko'a gi ge ko'a kloje pa ka ce'u bu'a ce'u ce'u ku 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 | ||
| Theorem | sezni-elt 577* | The identity element of monoids is unique. (Contributed by la korvo, 16-Oct-2024.) |
| ⊢ pa
ka ce'u bu'a
ce'u ce'u ku 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 | ||
| Syntax | sbdukni 578 |
|
| selbri dukni | ||
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 604 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. | ||
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. | ||
| Syntax | sli 579 |
|
| sumti li ku'i'a | ||
| Syntax | p0 580 |
|
| PA no | ||
| Theorem | sl0 581 | Syntax for zero. (Contributed by la korvo, 31-Jul-2024.) |
| sumti li no | ||
| Syntax | mbaihei 582 |
|
| PA bai'ei ku'i'a | ||
| Axiom | ax-baihei-inj 583* | 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 | ||
| Theorem | baihei-inj 584* | Inference form of ax-baihei-inj 583 (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 | ||
| Syntax | bkaclihe 585 |
|
| selbri kacli'e | ||
| Definition | df-kaclihe 586 | 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 | ||
| Axiom | ax-succ-zero 587 | Zero is not a successor. A standard axiom of second-order arithmetic. |
| ⊢ naku ko'a kacli'e li no | ||
| Theorem | succ-zero-ref 588 | Refutation of any claimed predecessor to zero. (Contributed by la korvo, 20-Aug-2023.) |
| ⊢ ko'a kacli'e li
no ⊢ gai'o | ||
| Syntax | p1 589 |
|
| PA pa | ||
| Theorem | sl1 590 | Syntax for one. (Contributed by la korvo, 31-Jul-2024.) |
| sumti li pa | ||
| Definition | df-pa 591 | One is the successor of zero. |
| ⊢ li pa du li bai'ei no | ||
| Syntax | p2 592 |
|
| PA re | ||
| Theorem | sl2 593 | Syntax for two. (Contributed by la korvo, 31-Jul-2024.) |
| sumti li re | ||
| Definition | df-re 594 | Two is the successor of one. |
| ⊢ li re du li bai'ei pa | ||
| Syntax | bkacnahu 595 |
|
| selbri kacna'u | ||
| Axiom | ax-nat-no 596 | Zero is a natural number. A standard axiom of second-order arithmetic. |
| ⊢ li no kacna'u | ||
| Axiom | ax-nat-pa 597 | One is a natural number. |
| ⊢ li pa kacna'u | ||
| Axiom | ax-succ-succ 598 | 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 583 |
| ⊢ ganai ko'a .e ko'e kacli'e ko'i gi ko'a du ko'e | ||
| Theorem | succ-succi 599 | Inference form of ax-succ-succ 598 (Contributed by la korvo, 7-Jul-2024.) |
| ⊢ ko'a .e ko'e
kacli'e ko'i ⊢ ko'a du ko'e | ||
| Axiom | ax-nat-ind 600* | 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 | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |