![]() |
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-fatci 501 | Definition of {fatci} in terms of {du'u}. |
⊢ go pa du'u broda kei fatci gi broda | ||
Theorem | fatcii 502 | Inference form of df-fatci 501 (Contributed by la korvo, 10-Mar-2024.) |
⊢ pa
du'u broda kei fatci ![]() | ||
Theorem | fatciri 503 | Reverse inference form of df-fatci 501 (Contributed by la korvo, 10-Mar-2024.) |
⊢ broda ![]() | ||
Theorem | fatci-ceihi 504 | {cei'i} is absolutely true when abstracted. (Contributed by la korvo, 10-Mar-2024.) |
⊢ pa du'u cei'i kei fatci | ||
Syntax | sbnibli 505 |
|
selbri nibli | ||
Definition | df-nibli 506 | {nibli} internalizes implication. |
⊢ go pa du'u broda kei nibli pa du'u brode kei gi ganai broda gi brode | ||
Theorem | niblii 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 ![]() | ||
Theorem | nibliii 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 ![]() ![]() | ||
Theorem | nibliri 509 | Reverse inference form of df-nibli 506 (Contributed by la korvo, 19-Jul-2024.) |
⊢ ganai broda gi brode ![]() | ||
Theorem | nibli-refl 510 | {nibli} is reflexive. (Contributed by la korvo, 19-Jul-2024.) |
⊢ pa du'u broda kei nibli pa du'u broda kei | ||
Syntax | sbsigda 511 |
|
selbri sigda | ||
Definition | df-sigda 512 | {sigda} internalizes implication. |
⊢ pa du'u ganai broda gi brode kei sigda pa du'u broda kei pa du'u brode kei | ||
Syntax | sbtsida 513 |
|
selbri tsida | ||
Definition | df-tsida 514 | {tsida} internalizes biimplication. |
⊢ pa du'u go broda gi brode kei tsida pa du'u broda kei pa du'u brode kei | ||
Syntax | sbkanxe 515 |
|
selbri kanxe | ||
Definition | df-kanxe 516 | {kanxe} internalizes conjunction. |
⊢ pa du'u ge broda gi brode kei kanxe pa du'u broda kei pa du'u brode kei | ||
Syntax | sbvlina 517 |
|
selbri vlina | ||
Definition | df-vlina 518 | {vlina} internalizes disjunction. |
⊢ pa du'u ga broda gi brode kei vlina pa du'u broda kei pa du'u brode kei | ||
Syntax | sbnalti 519 |
|
selbri nalti | ||
Definition | df-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 | ||
Definition | df-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 | ||
Syntax | sfahu 522 |
|
sumti ko'a fa'u ko'e | ||
Definition | df-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 | ||
Theorem | fahui 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 ![]() | ||
Theorem | fahuil 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 ![]() | ||
Theorem | fahuir 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 ![]() | ||
Theorem | fahuri 527 | Reverse inference form of df-fahu 523 (Contributed by la korvo, 16-Jun-2024.) |
⊢ ko'a bu'a ko'i ![]() ![]() | ||
Syntax | sziho 528 |
|
sumti zi'o | ||
Definition | df-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 | ||
Theorem | zihoi 530 | Inference form of df-ziho 529 (Contributed by la korvo, 22-Aug-2024.) |
⊢ ko'a bo'a ![]() | ||
Theorem | zihoit 531 | Delete the second place of a binary bridi. (Contributed by la korvo, 22-Aug-2024.) |
⊢ ko'a bu'a ko'e ![]() | ||
Theorem | zihogi 532 | First-order generalization of zihoi 530 (Contributed by la korvo, 12-Jul-2025.) |
⊢ ro da zo'u da
bo'a ![]() | ||
We investigate several common non-familial properties of relations. | ||
Syntax | sbtakni 533 |
|
selbri takni | ||
Definition | df-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 | ||
Theorem | taknii 535* | Inference form of df-takni 534 (Contributed by la korvo, 22-Jun-2024.) |
⊢ ko'a takni ko'e ![]() | ||
Syntax | sbkinfi 536 |
|
selbri kinfi | ||
Definition | df-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 | ||
Theorem | kinfiri 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 ![]() | ||
Syntax | sbkinra 539 |
|
selbri kinra | ||
Definition | df-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 | ||
Theorem | kinrari 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 ![]() | ||
Theorem | refl-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 ![]() | ||
Theorem | du-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 | ||
Theorem | gripau-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 | ||
Syntax | sbefklipi 545 |
|
selbri efklipi | ||
Syntax | sbefklizu 546 |
|
selbri efklizu | ||
Definition | df-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 | ||
Definition | df-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 | ||
Axiom | ax-efklipi-sym 549 | Every Euclidean reflexive relation is symmetric. |
⊢ ganai ko'a kinra je efklipi ko'e gi ko'a kinfi ko'e | ||
Axiom | ax-efklizu-sym 550 |
|
⊢ ganai ko'a kinra je efklizu ko'e gi ko'a kinfi ko'e | ||
Syntax | bpd 551 | Syntax for uniqueness quantification. |
bridi pa da zo'u broda | ||
Definition | df-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 | ||
Theorem | pa-dai 553 | Inference form of pa-da (future) (Contributed by la korvo, 20-Aug-2023.) |
⊢ pa
da zo'u da bo'a ![]() | ||
Theorem | pa-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 ![]() | ||
Syntax | bpdp 555 | Restriction for first-order uniqueness quantification. |
bridi pa da poi ke'a bo'a ku'o zo'u broda | ||
Definition | df-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 | ||
Theorem | poi-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 ![]() | ||
Theorem | poi-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 ![]() | ||
Syntax | sbpombo 559 |
|
selbri pombo | ||
Definition | df-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 | ||
Theorem | pomboi 561 | Inference form of df-pombo 560 (Contributed by la korvo, 8-Jul-2025.) |
⊢ ko'a pombo ko'e ![]() | ||
Theorem | pombori 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 ![]() | ||
Syntax | sbklojere 563 |
|
selbri klojere | ||
Definition | df-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 | ||
Syntax | sbkloje 565 |
|
selbri kloje | ||
Definition | df-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 | ||
Syntax | sbcajni 567 |
|
selbri cajni | ||
Definition | df-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 | ||
Syntax | sbsezni 569 |
|
selbri sezni | ||
Definition | df-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 | ||
Theorem | sezni-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 ![]() ![]() | ||
Syntax | sbdukni 572 |
|
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 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. | ||
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 573 |
|
sumti li ku'i'a | ||
Syntax | p0 574 |
|
PA no | ||
Theorem | sl0 575 | Syntax for zero. (Contributed by la korvo, 31-Jul-2024.) |
sumti li no | ||
Syntax | mbaihei 576 |
|
PA bai'ei ku'i'a | ||
Axiom | ax-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 | ||
Theorem | baihei-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 ![]() | ||
Syntax | bkaclihe 579 |
|
selbri kacli'e | ||
Definition | df-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 | ||
Axiom | ax-succ-zero 581 | Zero is not a successor. A standard axiom of second-order arithmetic. |
⊢ naku ko'a kacli'e li no | ||
Theorem | succ-zero-ref 582 | Refutation of any claimed predecessor to zero. (Contributed by la korvo, 20-Aug-2023.) |
⊢ ko'a kacli'e li
no ![]() | ||
Syntax | p1 583 |
|
PA pa | ||
Theorem | sl1 584 | Syntax for one. (Contributed by la korvo, 31-Jul-2024.) |
sumti li pa | ||
Definition | df-pa 585 | One is the successor of zero. |
⊢ li pa du li bai'ei no | ||
Syntax | p2 586 |
|
PA re | ||
Theorem | sl2 587 | Syntax for two. (Contributed by la korvo, 31-Jul-2024.) |
sumti li re | ||
Definition | df-re 588 | Two is the successor of one. |
⊢ li re du li bai'ei pa | ||
Syntax | bkacnahu 589 |
|
selbri kacna'u | ||
Axiom | ax-nat-no 590 | Zero is a natural number. A standard axiom of second-order arithmetic. |
⊢ li no kacna'u | ||
Axiom | ax-nat-pa 591 | One is a natural number. |
⊢ li pa kacna'u | ||
Axiom | ax-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 | ||
Theorem | succ-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 ![]() | ||
Axiom | ax-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 | ||
Theorem | nat-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 ![]() | ||
Theorem | nat-indii 596* | Inference form of ax-nat-ind 594 (Contributed by la korvo, 10-Aug-2023.) |
⊢ li no bo'a ![]() ![]() | ||
Theorem | nat-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 | ||
Axiom | ax-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 | ||
Syntax | msuhi 599* |
|
PA su'i ku'i'a ku'i'e | ||
Axiom | ax-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 > |
Copyright terms: Public domain | < Previous Next > |