HomeTheorem List (p. 5 of 11)
Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List
| Home |
brismu
bridi Theorem List (p. 5 of 11) |
< Previous Next >
|
|
Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List | ||
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | te-dual 401* | Self-duality property for {te}. (Contributed by la korvo, 13-Aug-2024.) |
⊢ ko'a bu'a naja
bu'e ko'e ko'i  ⊢ ko'i te bu'a
naja te bu'e ko'e ko'a | ||
| Theorem | te-dual-l 402* | Shift {te} to the left of an implication. (Contributed by la korvo, 13-Aug-2024.) |
| ⊢ ko'a bu'a naja
te bu'e ko'e ko'i ⊢ ko'i te bu'a
naja bu'e ko'e ko'a | ||
| Theorem | te-dual-r 403* | Shift {te} to the right of an implication. (Contributed by la korvo, 13-Aug-2024.) |
| ⊢ ko'a te bu'a
naja bu'e ko'e ko'i ⊢ ko'i bu'a naja
te bu'e ko'e ko'a | ||
| Theorem | te-ganaii 404* | Convert selbri on both sides of an implication simultaneously. (Contributed by la korvo, 13-Aug-2024.) |
| ⊢ ganai ko'a bu'a ko'e ko'i gi
fo'a bu'e fo'e fo'i ⊢ ganai
ko'i te bu'a ko'e ko'a gi fo'i
te bu'e fo'e fo'a | ||
| Theorem | te-ganair 405* | Convert selbri on both sides of an implication simultaneously. (Contributed by la korvo, 13-Aug-2024.) |
| ⊢ ganai ko'a te bu'a
ko'e ko'i
gi fo'a te bu'e fo'e fo'i ⊢ ganai
ko'i bu'a ko'e ko'a gi
fo'i bu'e fo'e fo'a | ||
| Syntax | sce 406 |
|
| sumti ko'a ce ko'e | ||
| Definition | df-ce 407 | Tentative definition of {ce}. |
| ⊢ go ko'a cmima ko'e ce ko'i gi ga ko'a du ko'e gi ko'a du ko'i | ||
| Theorem | cei 408 | Inference form of df-ce 407 (Contributed by la korvo, 5-Aug-2023.) |
| ⊢ ko'a cmima ko'e ce ko'i ⊢ ga
ko'a du ko'e gi ko'a
du ko'i | ||
| Theorem | ceri 409 | Reverse inference form of df-ce 407 (Contributed by la korvo, 5-Aug-2023.) |
| ⊢ ga ko'a du ko'e gi ko'a
du ko'i ⊢ ko'a cmima ko'e ce ko'i | ||
| Theorem | ceri-lin 410 | Inference from composition of ga-lin 165 and ceri 409 (Contributed by la korvo, 5-Aug-2023.) |
| ⊢ ko'a du ko'e ⊢ ko'a cmima ko'e ce ko'i | ||
| Theorem | ceri-rin 411 | Inference from composition of ga-rin 166 and ceri 409 (Contributed by la korvo, 5-Aug-2023.) |
| ⊢ ko'a du ko'i ⊢ ko'a cmima ko'e ce ko'i | ||
| Theorem | ce-left 412 | Assertion for left-hand component of a {ce} union. (Contributed by la korvo, 5-Aug-2023.) |
| ⊢ ko'a cmima ko'a ce ko'e | ||
| Theorem | ce-right 413 | Assertion for right-hand component of a {ce} union. (Contributed by la korvo, 5-Aug-2023.) |
| ⊢ ko'e cmima ko'a ce ko'e | ||
| Syntax | bsd 414 | Syntax for first-order existential quantification. |
| bridi su'o da zo'u broda | ||
| Syntax | bsb 415 | Syntax for second-order existential quantification. |
| bridi su'o bu'a zo'u broda | ||
| Axiom | ax-ex 416 | The axiom of existence: at least one element exists in the universe. This is necessary if we want to exclude the trivial empty model. The apparent mismatch between metavariable types is required in order to evade the global distinctness requirement; this axiom holds even if {da} and {ko'a} are syntactically equivalent. |
| ⊢ su'o da zo'u da du ko'a | ||
| Theorem | exv 417* | A weaker version of ax-ex 416 which requires {da} and {de} to be distinct. (Contributed by la korvo, 4-Jan-2025.) |
| ⊢ su'o da zo'u da du de | ||
| Axiom | ax-eb 418 | {su'o da zo'u} binds {da}. |
| ⊢ ganai su'o da zo'u broda gi ro da zo'u su'o da zo'u broda | ||
| Theorem | ebi 419 | Inference form of ax-eb 418 (Contributed by la korvo, 22-Jun-2024.) |
| ⊢ su'o da zo'u broda ⊢ ro
da zo'u su'o da zo'u broda | ||
| Axiom | ax-eq 420 | Extensional definition of existential quantification in terms of universal quantification. |
| ⊢ ganai ro da zo'u ganai broda gi ro da zo'u broda gi go ro da zo'u ganai brode gi broda gi ganai su'o da zo'u brode gi broda | ||
| Theorem | eqi 421 | Inference form of ax-eq 420 (Contributed by la korvo, 22-Jun-2024.) |
| ⊢ ro da zo'u ganai broda gi ro da zo'u broda ⊢ go
ro da zo'u
ganai brode gi broda gi ganai
su'o da zo'u brode gi broda | ||
| Theorem | eqih 422 | Reduced inference from ax-eq 420 (Contributed by la korvo, 22-Jun-2024.) |
| ⊢ ganai broda gi ro da zo'u broda ⊢ go
ro da zo'u
ganai brode gi broda gi ganai
su'o da zo'u brode gi broda | ||
| Theorem | wit 423 | Due to ax-ex 416 there will always be a spurious witness to any true bridi. (Contributed by la korvo, 23-Jun-2024.) |
| ⊢ ganai broda gi su'o da zo'u broda | ||
| Theorem | exlimih 424 | Convert universal quantification to existential quantification on top of an inference. (Contributed by la korvo, 9-Jul-2025.) |
⊢ ganai brode gi ro da zo'u brode  ⊢ ganai
broda gi brode ⊢ ganai
su'o da zo'u broda gi brode | ||
| Theorem | exlimdh 425 | Deduction converting universal quantification to existential quantification. (Contributed by la korvo, 9-Jul-2025.) |
| ⊢ ganai broda gi ro da zo'u broda ⊢ ganai
brodi gi ro da zo'u brodi ⊢ ganai
broda gi ganai brode gi brodi ⊢ ganai
broda gi ganai
su'o da zo'u brode gi brodi | ||
| Theorem | exim 426 | Internalization of the concept that, if an arrow is inhabited for all values of some variable, then the existence of an inhabitant in the source of the arrow implies an inhabitant in the target of the arrow. (Contributed by la korvo, 9-Jul-2025.) |
| ⊢ ganai ro da zo'u ganai broda gi brode gi ganai su'o da zo'u broda gi su'o da zo'u brode | ||
| Theorem | eximi 427 | Inference form of exim 426 (Contributed by la korvo, 9-Jul-2025.) |
| ⊢ ganai broda gi brode ⊢ ganai
su'o da zo'u broda gi su'o da zo'u brode | ||
| Theorem | eximdh 428 | Deductive form of exim 426 (Contributed by la korvo, 9-Jul-2025.) |
| ⊢ ganai broda gi ro da zo'u broda ⊢ ganai
broda gi ganai brode gi brodi ⊢ ganai
broda gi ganai
su'o da zo'u brode gi su'o da zo'u brodi | ||
| Theorem | foml19.29 429 | Theorem 19.29 of [Margaris] p. 90. (Contributed by la korvo, 9-Jul-2025.) |
| ⊢ ganai ge ro da zo'u broda gi su'o da zo'u brode gi su'o da zo'u ge broda gi brode | ||
| Theorem | ge-lex 430 | Universal property of products ax-ge-le 48 underneath existential quantification. (Contributed by la korvo, 9-Jul-2025.) |
| ⊢ ganai su'o da zo'u ge broda gi brode gi su'o da zo'u broda | ||
| Theorem | ge-dist-ex 431 | Distribute existential quantification over conjunction. Theorem 19.40 of [Margaris] p. 90. (Contributed by la korvo, 9-Jul-2025.) |
| ⊢ ganai su'o da zo'u ge broda gi brode gi ge su'o da zo'u broda gi su'o da zo'u brode | ||
| Theorem | foml19.41 432 | Obsolete version of theorem 19.41 of [Margaris] p. 90. (Contributed by la korvo, 9-Jul-2025.) |
| ⊢ ganai brode gi ro da zo'u brode ⊢ go
su'o da zo'u
ge broda gi brode gi ge
su'o da zo'u broda gi brode | ||
| Axiom | ax-cmima-nul 433* | The Axiom of Null Set: there exists a set with no elements. |
| ⊢ su'o da zo'u ro de zo'u naku de cmima da | ||
| Syntax | bnd 434 | Syntax for first-order not-free quantification. |
| bridi na'a'u da zo'u broda | ||
| Definition | df-nahahu 435 | Definition of not-free quantification: {na'a'u da} means that the value which {da} takes on is effectively irrelevant to the truth value of its bridi. |
| ⊢ go na'a'u da zo'u broda gi ro da zo'u ganai broda gi ro da zo'u broda | ||
| Theorem | bi-revg 436 | bi-rev 102 with generalization on the RHS. (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ go broda gi ro da zo'u brode ⊢ brode ⊢ broda | ||
| Theorem | nfi 437 | Inference form of df-nahahu 435 (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ ganai broda gi ro da zo'u broda ⊢
na'a'u da zo'u broda | ||
| Theorem | nfr 438 | Property of not-free quantification. (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ ganai na'a'u da zo'u broda gi ganai broda gi ro da zo'u broda | ||
| Theorem | nfri 439 | Inference form of nfr 438 (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ na'a'u da zo'u broda ⊢ ganai
broda gi ro da zo'u broda | ||
| Theorem | hbth 440 | Hypothesis builder: theorems are closed. (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ broda ⊢ ganai
broda gi ro da zo'u broda | ||
| Theorem | nfth 441 | Theorems are closed. (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ broda ⊢
na'a'u da zo'u broda | ||
| Theorem | nfnth 442 | Non-theorems are closed. (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ naku broda ⊢
na'a'u da zo'u broda | ||
| Theorem | ceihi-nf 443 | The true relation is closed. (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ na'a'u da zo'u cei'i | ||
| Axiom | ax-dgen1 444* | Special case of first-order generalization where the quantified variable does not occur in the bridi. |
| ⊢ ganai broda gi ro da zo'u broda | ||
| Theorem | nfv 445* | If a variable does not occur in a bridi, then it is neither free nor bound in that bridi. (Contributed by la korvo, 3-Jan-2025.) |
| ⊢ na'a'u da zo'u broda | ||
| Syntax | bsub 446 | Metasyntax for substitutions. In this example, we are replacing every instance of {da} within {broda} with {ko'a}. |
| bridi [ ko'a / da ] broda | ||
| Definition | df-sub 447 | Definition of proper substitution following definition df-sb in [ILE] p. 0. This clever gadget breaks scoping to require that substitution is correct in both the case where {da} is free and the case where {da} is bound by mixing both cases, skipping grammatical analysis and scope-tracking entirely. |
| ⊢ go [ ko'a / da ] broda gi ge ganai da du ko'a gi broda gi su'o da zo'u ge da du ko'a gi broda | ||
| Theorem | subi 448 | Inference form of df-sub 447 (Contributed by la korvo, 22-Jun-2024.) |
| ⊢ [ ko'a / da ] broda ⊢ ge
ganai da du ko'a gi
broda gi su'o da zo'u ge da du ko'a gi broda | ||
| Theorem | sub1 449 | Property of proper substitution. (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ ganai [ ko'a / da ] broda gi su'o da zo'u ge da du ko'a gi broda | ||
| Theorem | subeq-lem1 450 |
|
| ⊢ ganai da du ko'a gi ganai broda gi [ ko'a / da ] broda | ||
| Theorem | subeq-lem2 451 |
|
| ⊢ ganai da du ko'a gi ganai [ ko'a / da ] broda gi broda | ||
| Theorem | subid 452 | An identity for substitutions. (Contributed by la korvo, 22-Jun-2024.) |
| ⊢ go [ da / da ] broda gi broda | ||
| Theorem | equs4 453 | A lemma for substitutions. (Contributed by la korvo, 9-Jul-2025.) |
| ⊢ ganai ro da zo'u ganai da du ko'a gi broda gi su'o da zo'u ge da du ko'a gi broda | ||
| Theorem | sub2 454 | Property of proper substitution. (Contributed by la korvo, 9-Jul-2025.) |
| ⊢ ganai ro da zo'u ganai da du ko'a gi broda gi [ ko'a / da ] broda | ||
| Theorem | stdpc4 455 | The Axiom of Specialization: if a statement holds for all values, then it holds when substituted for any particular value. (Contributed by la korvo, 9-Jul-2025.) |
| ⊢ ganai ro da zo'u broda gi [ ko'a / da ] broda | ||
| Theorem | subh 456 | Variables which are not free can be substituted. (Contributed by la korvo, 9-Jul-2025.) |
| ⊢ ganai broda gi ro da zo'u broda ⊢ go [
ko'a / da ] broda gi broda | ||
| Theorem | subf 457 | Variables which are not free can be substituted. (Contributed by la korvo, 9-Jul-2025.) |
| ⊢ na'a'u da zo'u broda ⊢ go [
ko'a / da ] broda gi broda | ||
| Theorem | subt 458 | Theorems are invariant under substitution. (Contributed by la korvo, 9-Jul-2025.) |
| ⊢ broda ⊢ [ ko'a / da ] broda | ||
| Syntax | sbzilcmi 459 |
|
| selbri zilcmi | ||
| Definition | df-zilcmi 460 | {zilcmi} is lujvo for {se cmima zi'o}. The effect is to include {le nomei} as a valid set, forming a predicate of possibly-inhabited sets. |
| ⊢ go ko'a zilcmi gi ga ko'a du le nomei ku gi su'o da zo'u da cmima ko'a | ||
| Theorem | zilcmi-nomei 461 | The empty set is a set. (Contributed by la korvo, 19-Sep-2024.) |
| ⊢ le nomei ku zilcmi | ||
| Theorem | cmima-zilcmi 462 | Forget the inhabitant of a set. (Contributed by la korvo, 19-Sep-2024.) |
| ⊢ su'o da zo'u da
cmima ko'a ⊢ ko'a zilcmi | ||
| Syntax | brdp 463 | Restriction for first-order universal quantification. |
| bridi ro da poi ke'a bo'a ku'o zo'u broda | ||
| Syntax | bsdp 464 | Restriction for first-order universal quantification. |
| bridi su'o da poi ke'a bo'a ku'o zo'u broda | ||
| Definition | df-poi-ro 465 | Definition of {ro da poi} quantifiers as restricted first-order universal quantifiers. |
| ⊢ go ro da poi ke'a bo'a ku'o zo'u broda gi ro da zo'u ganai da bo'a gi broda | ||
| Theorem | poi-roi 466 | Inference form of df-poi-ro 465 (Contributed by la korvo, 11-Aug-2023.) |
| ⊢ ro da poi ke'a bo'a ku'o zo'u broda ⊢ ro
da zo'u ganai da bo'a gi
broda | ||
| Theorem | poi-rori 467 | Reverse inference form of df-poi-ro 465 (Contributed by la korvo, 11-Aug-2023.) |
| ⊢ ro da zo'u ganai da bo'a gi
broda ⊢
ro da poi
ke'a bo'a ku'o
zo'u broda | ||
| Theorem | poi-gen 468 | First-order generalization for restricted quantification. (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ broda ⊢ ro
da poi ke'a bo'a ku'o zo'u broda | ||
| Theorem | ro-poi 469 | Restricted quantification is a special case of universal quantification. (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ ro da zo'u broda ⊢ ro
da poi ke'a bo'a ku'o zo'u broda | ||
| Syntax | brbc 470* |
|
| bridi ro bu'a cu bu'e | ||
| Definition | df-ro-quant 471* | Definition of {ro broda} quantifier as used in colloquial Lojban utterances like {ro broda cu brode}. |
| ⊢ go ro bu'a cu bu'e gi ro da poi ke'a bu'a ku'o zo'u da bu'e | ||
| Theorem | ro-quanti 472* | Inference form of df-ro-quant 471 (Contributed by la korvo, 12-Sep-2023.) |
| ⊢ ro bu'a cu bu'e ⊢ ro
da poi ke'a bu'a ku'o zo'u da bu'e | ||
| Theorem | ro-quantri 473* | Reverse inference form of df-ro-quant 471 (Contributed by la korvo, 12-Sep-2023.) |
| ⊢ ro da poi ke'a bu'a ku'o zo'u da bu'e ⊢ ro bu'a cu bu'e | ||
| Axiom | ax-cmima-coll 474* | The Axiom of Collection: If a bridi is inhabited when parameterized over elements of some set, then the inhabitants also form a set. |
| ⊢ na'a'u da zo'u broda ⊢ ganai
ro de poi
ke'a cmima ko'a ku'o zo'u
su'o di zo'u broda gi su'o da zo'u ro de poi ke'a cmima ko'a ku'o
zo'u su'o di
poi ke'a cmima da ku'o zo'u broda | ||
| Syntax | brdpu 475 | Restriction for first-order identity. |
| bridi ro da po'u ko'a zo'u broda | ||
| Definition | df-pohu 476 | Definition of {po'u} in terms of {poi du}, as given by example 3.9-10 from [CLL] p. 8. |
| ⊢ go ro da po'u ko'a zo'u broda gi ro da poi ke'a du ko'a ku'o zo'u broda | ||
| Syntax | sbkampu 477 |
|
| selbri kampu | ||
| Definition | df-kampu 478 | Definition of {kampu} in terms of {ckaji} and {cmima}. |
| ⊢ go ko'a kampu ko'e gi ro da poi ke'a cmima ko'e ku'o zo'u da ckaji ko'a | ||
| Theorem | kampui 479 | Inference form of df-kampu 478 (Contributed by la korvo, 17-Aug-2023.) |
| ⊢ ko'a kampu ko'e ⊢ ro
da poi ke'a cmima ko'e ku'o
zo'u da ckaji ko'a | ||
| Theorem | kampuri 480 | Reverse inference form of df-kampu 478 (Contributed by la korvo, 17-Aug-2023.) |
| ⊢ ro da poi ke'a cmima ko'e ku'o
zo'u da ckaji ko'a ⊢ ko'a kampu ko'e | ||
| Syntax | sjohe 481 |
|
| sumti ko'a jo'e ko'e | ||
| Definition | df-johe 482 | Definition of {jo'e} in terms of {ga}. |
| ⊢ go ko'a cmima ko'e jo'e ko'i gi ko'a cmima ko'e .a ko'i | ||
| Theorem | johei 483 | Inference form of df-johe 482 (Contributed by la korvo, 22-Aug-2023.) |
| ⊢ ko'a cmima ko'e jo'e ko'i ⊢ ko'a cmima ko'e .a ko'i | ||
| Theorem | joheri 484 | Reverse inference form of df-johe 482 (Contributed by la korvo, 22-Aug-2023.) |
| ⊢ ko'a cmima ko'e .a ko'i ⊢ ko'a cmima ko'e jo'e ko'i | ||
| Syntax | skuha 485 |
|
| sumti ko'a ku'a ko'e | ||
| Definition | df-kuha 486 | Definition of {ku'a} in terms of {ge}. |
| ⊢ go ko'a cmima ko'e ku'a ko'i gi ko'a cmima ko'e .e ko'i | ||
| Theorem | kuhai 487 | Inference form of df-kuha 486 (Contributed by la korvo, 22-Aug-2023.) |
| ⊢ ko'a cmima ko'e ku'a ko'i ⊢ ko'a cmima ko'e .e ko'i | ||
| Theorem | kuhari 488 | Reverse inference form of df-kuha 486 (Contributed by la korvo, 22-Aug-2023.) |
| ⊢ ko'a cmima ko'e .e ko'i ⊢ ko'a cmima ko'e ku'a ko'i | ||
The abstractor {du'u} contains any {ka} abstractions which are closed. Our reasoning for {pa ka} quantification extends to {pa du'u} quantification. | ||
| Syntax | sdu 489 | If {broda} is a bridi, then {pa du'u} captures it as a sumti. |
| sumti pa du'u broda kei | ||
| Syntax | sceho 490 |
|
| sumti ko'a ce'o ko'e | ||
| Syntax | sbbridi 491 |
|
| selbri bridi | ||
| Definition | df-bridi-u 492 |
|
| ⊢ pa du'u ko'a bu'a kei bridi pa ka ce'u bu'a kei ko'a | ||
| Definition | df-bridi-b 493 |
|
| ⊢ pa du'u ko'a bu'a ko'e kei bridi pa ka ce'u bu'a ce'u kei ko'a ce'o ko'e | ||
| Definition | df-bridi-t 494 |
|
| ⊢ pa du'u ko'a bu'a ko'e ko'i kei bridi pa ka ce'u bu'a ce'u ce'u kei ko'a ce'o ko'e ce'o ko'i | ||
| Definition | df-bridi-q 495 |
|
| ⊢ pa du'u ko'a bu'a ko'e ko'i ko'o kei bridi pa ka ce'u bu'a ce'u ce'u ce'u kei ko'a ce'o ko'e ce'o ko'i ce'o ko'o | ||
| Syntax | sbselbri 496 |
|
| selbri selbri | ||
| Definition | df-selbri 497 |
|
| ⊢ go ko'a selbri ko'e ko'i gi ko'a se bridi ko'e ko'i | ||
| Theorem | selbrii 498 | Inference form of df-selbri 497 (Contributed by la korvo, 15-Jun-2025.) |
| ⊢ ko'a selbri ko'e
ko'i ⊢ ko'a se bridi
ko'e ko'i | ||
| Theorem | selbriri 499 | Reverse inference form of df-selbri 497 (Contributed by la korvo, 15-Jun-2025.) |
| ⊢ ko'a se bridi
ko'e ko'i ⊢ ko'a selbri ko'e
ko'i | ||
| Syntax | sbfatci 500 |
|
| selbri fatci | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |