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 | teri 401 | Reverse inference form of df-te 399 (Contributed by la korvo, 18-Jul-2023.) |
⊢ ko'a bu'a ko'e ko'i  ⊢ ko'i te bu'a
ko'e ko'a | ||
| Theorem | te-invo 402 | {te} is an involution. (Contributed by la korvo, 18-Jul-2023.) |
| ⊢ ko'a te te bu'a ko'e ko'i ⊢ ko'a bu'a ko'e ko'i | ||
| Theorem | te-dual 403* | 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 404* | 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 405* | 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 406* | 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 407* | 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 408 |
|
| sumti ko'a ce ko'e | ||
| Definition | df-ce 409 | 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 410 | Inference form of df-ce 409 (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 411 | Reverse inference form of df-ce 409 (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 412 | Inference from composition of ga-lin 165 and ceri 411 (Contributed by la korvo, 5-Aug-2023.) |
| ⊢ ko'a du ko'e ⊢ ko'a cmima ko'e ce ko'i | ||
| Theorem | ceri-rin 413 | Inference from composition of ga-rin 166 and ceri 411 (Contributed by la korvo, 5-Aug-2023.) |
| ⊢ ko'a du ko'i ⊢ ko'a cmima ko'e ce ko'i | ||
| Theorem | ce-left 414 | 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 415 | 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 416 | Syntax for first-order existential quantification. |
| bridi su'o da zo'u broda | ||
| Syntax | bsb 417 | Syntax for second-order existential quantification. |
| bridi su'o bu'a zo'u broda | ||
| Axiom | ax-ex 418 | 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 419* | A weaker version of ax-ex 418 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 420 | {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 421 | Inference form of ax-eb 420 (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 422 | 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 423 | Inference form of ax-eq 422 (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 424 | Reduced inference from ax-eq 422 (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 425 | Due to ax-ex 418 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 426 | 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 427 | 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 428 | 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 429 | Inference form of exim 428 (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 430 | Deductive form of exim 428 (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 431 | 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 432 | 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 433 | 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 434 | 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 435* | 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 436 | Syntax for first-order not-free quantification. |
| bridi na'a'u da zo'u broda | ||
| Definition | df-nahahu 437 | 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 438 | 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 439 | Inference form of df-nahahu 437 (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ ganai broda gi ro da zo'u broda ⊢
na'a'u da zo'u broda | ||
| Theorem | nfr 440 | 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 441 | Inference form of nfr 440 (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ na'a'u da zo'u broda ⊢ ganai
broda gi ro da zo'u broda | ||
| Theorem | hbth 442 | Hypothesis builder: theorems are closed. (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ broda ⊢ ganai
broda gi ro da zo'u broda | ||
| Theorem | nfth 443 | Theorems are closed. (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ broda ⊢
na'a'u da zo'u broda | ||
| Theorem | nfnth 444 | Non-theorems are closed. (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ naku broda ⊢
na'a'u da zo'u broda | ||
| Theorem | ceihi-nf 445 | The true relation is closed. (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ na'a'u da zo'u cei'i | ||
| Axiom | ax-dgen1 446* | 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 447* | 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 448 | 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 449 | 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 450 | Inference form of df-sub 449 (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 451 | 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 452 |
|
| ⊢ ganai da du ko'a gi ganai broda gi [ ko'a / da ] broda | ||
| Theorem | subeq-lem2 453 |
|
| ⊢ ganai da du ko'a gi ganai [ ko'a / da ] broda gi broda | ||
| Theorem | subid 454 | An identity for substitutions. (Contributed by la korvo, 22-Jun-2024.) |
| ⊢ go [ da / da ] broda gi broda | ||
| Theorem | equs4 455 | 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 456 | 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 | subequ2 457 | Use an equality to remove a substitution. (Contributed by la korvo, 11-Aug-2026.) |
| ⊢ ganai da du ko'a gi ganai [ ko'a / da ] broda gi broda | ||
| Theorem | stdpc4 458 | 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 | stdpc6 459 | An axiom of equality for predicate calculus. (Contributed by la korvo, 11-Aug-2026.) |
| ⊢ ro da zo'u da du da | ||
| Theorem | stdpc7 460 | An axiom of equality for predicate calculus. (Contributed by la korvo, 11-Aug-2026.) |
| ⊢ ganai ko'a du da gi ganai [ ko'a / da ] broda gi broda | ||
| Theorem | subh 461 | 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 462 | 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 463 | Theorems are invariant under substitution. (Contributed by la korvo, 9-Jul-2025.) |
| ⊢ broda ⊢ [ ko'a / da ] broda | ||
| Syntax | sbzilcmi 464 |
|
| selbri zilcmi | ||
| Definition | df-zilcmi 465 | {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 466 | The empty set is a set. (Contributed by la korvo, 19-Sep-2024.) |
| ⊢ le nomei ku zilcmi | ||
| Theorem | cmima-zilcmi 467 | 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 | ||
| Theorem | selcmi-zilcmi 468 | Inhabited sets are sets. (Contributed by la korvo, 19-Sep-2024.) |
| ⊢ ko'e cmima ko'a ⊢ ko'a zilcmi | ||
| Syntax | brdp 469 | Restriction for first-order universal quantification. |
| bridi ro da poi ke'a bo'a ku'o zo'u broda | ||
| Syntax | bsdp 470 | Restriction for first-order universal quantification. |
| bridi su'o da poi ke'a bo'a ku'o zo'u broda | ||
| Definition | df-poi-ro 471 | 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 472 | Inference form of df-poi-ro 471 (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 473 | Reverse inference form of df-poi-ro 471 (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 474 | 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 475 | 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 476* |
|
| bridi ro bu'a cu bu'e | ||
| Definition | df-ro-quant 477* | 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 478* | Inference form of df-ro-quant 477 (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 479* | Reverse inference form of df-ro-quant 477 (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 480* | 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 481 | Restriction for first-order identity. |
| bridi ro da po'u ko'a zo'u broda | ||
| Definition | df-pohu 482 | 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 483 |
|
| selbri kampu | ||
| Definition | df-kampu 484 | 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 485 | Inference form of df-kampu 484 (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 486 | Reverse inference form of df-kampu 484 (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 487 |
|
| sumti ko'a jo'e ko'e | ||
| Definition | df-johe 488 | 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 489 | Inference form of df-johe 488 (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 490 | Reverse inference form of df-johe 488 (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 491 |
|
| sumti ko'a ku'a ko'e | ||
| Definition | df-kuha 492 | 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 493 | Inference form of df-kuha 492 (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 494 | Reverse inference form of df-kuha 492 (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 495 | If {broda} is a bridi, then {pa du'u} captures it as a sumti. |
| sumti pa du'u broda ku | ||
| Syntax | sceho 496 |
|
| sumti ko'a ce'o ko'e | ||
| Syntax | sbbridi 497 |
|
| selbri bridi | ||
| Definition | df-bridi-u 498 |
|
| ⊢ pa du'u ko'a bu'a ku bridi pa ka ce'u bu'a ku ko'a | ||
| Definition | df-bridi-b 499 |
|
| ⊢ pa du'u ko'a bu'a ko'e ku bridi pa ka ce'u bu'a ce'u ku ko'a ce'o ko'e | ||
| Definition | df-bridi-t 500 |
|
| ⊢ pa du'u ko'a bu'a ko'e ko'i ku bridi pa ka ce'u bu'a ce'u ce'u ku ko'a ce'o ko'e ce'o ko'i | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |