HomeTheorem List (p. 2 of 8)
Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List
| Home |
brismu
bridi Theorem List (p. 2 of 8) |
< Previous Next >
|
|
Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List | ||
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | nagihai 101 | Inference form of df-nagiha 100 (Contributed by la korvo, 17-Aug-2023.) |
⊢ ko'a bo'a
nagi'a bo'e  ⊢ ganai ko'a bo'a gi
ko'a bo'e | ||
| Theorem | nagihaii 102 | Inference form of df-nagiha 100 (Contributed by la korvo, 17-Aug-2023.) |
⊢ ko'a bo'a
nagi'a bo'e  ⊢ ko'a bo'a ⊢ ko'a bo'e | ||
| Theorem | nagihari 103 | Inference form of df-nagiha 100 (Contributed by la korvo, 17-Aug-2023.) |
| ⊢ ganai ko'a bo'a gi
ko'a bo'e ⊢ ko'a bo'a
nagi'a bo'e | ||
| Syntax | tgihanai 104 |
|
| brirebla bo'a gi'anai bo'e | ||
| Definition | df-gihanai 105 | Definition of {gi'anai} in terms of {ganai}. |
| ⊢ go ko'a bo'e gi'anai bo'a gi ganai ko'a bo'a gi ko'a bo'e | ||
| Theorem | gihanaii 106 | Inference form of df-gihanai 105 (Contributed by la korvo, 16-Aug-2023.) |
| ⊢ ko'a bo'e
gi'anai bo'a ⊢ ganai
ko'a bo'a
gi ko'a bo'e | ||
| Theorem | gihanaiii 107 | Inference form of df-gihanai 105 (Contributed by la korvo, 16-Aug-2023.) |
| ⊢ ko'a bo'e
gi'anai bo'a ⊢ ko'a bo'a ⊢ ko'a bo'e | ||
| Theorem | gihanairi 108 | Inference form of df-gihanai 105 (Contributed by la korvo, 16-Aug-2023.) |
| ⊢ ganai ko'a bo'e gi
ko'a bo'a ⊢ ko'a bo'a
gi'anai bo'e | ||
| Theorem | ge-com-lem 109 | Lemma for ge-com 110 showing that {ge} is commutative in one direction. (Contributed by la korvo, 31-Jul-2023.) [Auxiliary lemma - not displayed.] |
| Theorem | ge-com 110 | {ge} is commutative. (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ go ge broda gi brode gi ge brode gi broda | ||
| Theorem | ge-go 111 | Conjunction implies biimplication. (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ ge broda gi brode ⊢ go
broda gi brode | ||
| Theorem | ge-diag 112 | {ge} admits the diagonal morphism. (Contributed by la korvo, 21-Aug-2024.) |
| ⊢ ganai broda gi ge broda gi broda | ||
| Theorem | ge-idem 113 | {ge} is idempotent. (Contributed by la korvo, 15-Aug-2024.) (Strengthened by la korvo, 21-Aug-2024.) |
| ⊢ go ge broda gi broda gi broda | ||
| Syntax | sje 114 |
|
| sumti ko'a .e ko'e | ||
| Definition | df-e 115 | Definition of {.e} in terms of {ge}. Forethought version of example 12.2-5 from [CLL] p. 14. |
| ⊢ go ko'a .e ko'e bo'a gi ge ko'a bo'a gi ko'e bo'a | ||
| Theorem | ei 116 | Inference form of df-e 115 (Contributed by la korvo, 17-Jul-2023.) |
| ⊢ ko'a .e ko'e
bo'a ⊢
ge ko'a bo'a gi ko'e
bo'a | ||
| Theorem | eri 117 | Reverse inference form of df-e 115 (Contributed by la korvo, 17-Jul-2023.) |
| ⊢ ge ko'a bo'a gi
ko'e bo'a ⊢ ko'a .e ko'e
bo'a | ||
| Syntax | sbje 118* |
|
| selbri bu'a je bu'e | ||
| Definition | df-je 119* | Definition of {je} in terms of {ge}. From example 12.2-5 of [CLL] p. 14. |
| ⊢ go ko'a bu'a je bu'e ko'e gi ge ko'a bu'a ko'e gi ko'a bu'e ko'e | ||
| Theorem | jei 120* | Inference form of df-je 119 (Contributed by la korvo, 17-Jul-2023.) |
| ⊢ ko'a bu'a je
bu'e ko'e ⊢ ge
ko'a bu'a ko'e gi ko'a
bu'e ko'e | ||
| Theorem | jeri 121* | Reverse inference form of df-je 119 (Contributed by la korvo, 17-Jul-2023.) |
| ⊢ ge ko'a bu'a ko'e gi ko'a
bu'e ko'e ⊢ ko'a bu'a je
bu'e ko'e | ||
| Syntax | tgihe 122 |
|
| brirebla bo'a gi'e bo'e | ||
| Definition | df-gihe 123 | Definition of {gi'e} in terms of {ge}. |
| ⊢ go ko'a bo'a gi'e bo'e gi ge ko'a bo'a gi ko'a bo'e | ||
| Theorem | gihei 124 | Inference form of df-gihe 123 (Contributed by la korvo, 14-Aug-2023.) |
| ⊢ ko'a bo'a
gi'e bo'e ⊢ ge ko'a bo'a gi
ko'a bo'e | ||
| Theorem | giheri 125 | Inference form of df-gihe 123 (Contributed by la korvo, 14-Aug-2023.) |
| ⊢ ge ko'a bo'a gi
ko'a bo'e ⊢ ko'a bo'a
gi'e bo'e | ||
| Theorem | giherii 126 | Inference form of df-gihe 123 (Contributed by la korvo, 14-Aug-2023.) |
| ⊢ ko'a bo'a ⊢ ko'a bo'e ⊢ ko'a bo'a
gi'e bo'e | ||
Disjunctions are the first connective for which we can introduce all four forms simultaneously. The {ga} form is fundamental in our syntax, since it gives the best scoping; but we define all of the other forms so that we have them available for sugar later. | ||
| Syntax | bga 127 |
|
| bridi ga broda gi brode | ||
| Definition | df-ga 128 | Definition of {ga} in terms of {go}, {ganai}, and {ge}. Axiom ax-io in [ILE] p. 0. |
| ⊢ go ganai ga brode gi brodi gi broda gi ge ganai brode gi broda gi ganai brodi gi broda | ||
| Theorem | gai 129 | Inference form of df-ga 128 (Contributed by la korvo, 28-Jul-2023.) |
| ⊢ ganai
ga brode gi brodi gi broda ⊢ ge
ganai brode gi broda gi ganai brodi gi broda | ||
| Theorem | gar 130 | Reverse implication of df-ga 128 (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ ganai ge ganai brode gi broda gi ganai brodi gi broda gi ganai ga brode gi brodi gi broda | ||
| Theorem | gari 131 | Reverse inference form of df-ga 128 (Contributed by la korvo, 28-Jul-2023.) |
| ⊢ ge
ganai brode gi broda gi ganai brodi gi broda ⊢ ganai
ga brode gi brodi gi broda | ||
| Theorem | ga-lin 132 | Introduce {ga} with the antecedent on the left. Theorem orc in [ILE] p. 0. (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ ganai broda gi ga broda gi brode | ||
| Theorem | ga-rin 133 | Introduce {ga} with the antecedent on the right. Theorem olc in [ILE] p. 0. (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ ganai broda gi ga brode gi broda | ||
| Theorem | garii 134 | Nested inference form of gar 130 (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ ganai broda gi brode ⊢ ganai
brodi gi brode ⊢ ganai
ga broda gi brodi gi brode | ||
| Theorem | ga-idem 135 | {ga} is idempotent. (Contributed by la korvo, 15-Aug-2024.) |
| ⊢ go ga broda gi broda gi broda | ||
| Theorem | ga-com-lem 136 | Lemma for ga-com 137 (Contributed by la korvo, 31-Jul-2023.) [Auxiliary lemma - not displayed.] |
| Theorem | ga-com 137 | {ga} commutes. (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ go ga broda gi brode gi ga brode gi broda | ||
| Syntax | sja 138 |
|
| sumti ko'a .a ko'e | ||
| Definition | df-a 139 | Definition of {.a} in terms of {ga}. Forethought version of example 12.2-5 from [CLL] p. 14. |
| ⊢ go ko'a .a ko'e bo'a gi ga ko'a bo'a gi ko'e bo'a | ||
| Theorem | ai 140 | Inference form of df-a 139 (Contributed by la korvo, 14-Aug-2023.) |
| ⊢ ko'a .a ko'e
bo'a ⊢
ga ko'a bo'a gi ko'e
bo'a | ||
| Theorem | ari 141 | Inference form of df-a 139 (Contributed by la korvo, 14-Aug-2023.) |
| ⊢ ga ko'a bo'a gi
ko'e bo'a ⊢ ko'a .a ko'e
bo'a | ||
| Theorem | a-com 142 | {.a} commutes. (Contributed by la korvo, 17-Aug-2023.) |
| ⊢ go ko'a .a ko'e bo'a gi ko'e .a ko'a bo'a | ||
| Theorem | a-comi 143 | Inference form of a-com 142 |
| ⊢ ko'a .a ko'e
bo'a ⊢ ko'e .a ko'a
bo'a | ||
| Syntax | sbja 144* |
|
| selbri bu'a ja bu'e | ||
| Definition | df-ja 145* | Definition of {ja} in terms of {ga}. From example 12.2-5 of [CLL] p. 14. |
| ⊢ go ko'a bu'a ja bu'e ko'e gi ga ko'a bu'a ko'e gi ko'a bu'e ko'e | ||
| Theorem | jai 146* | Inference form of df-ja 145 (Contributed by la korvo, 16-Aug-2023.) |
| ⊢ ko'a bu'a ja
bu'e ko'e ⊢ ga
ko'a bu'a ko'e gi ko'a
bu'e ko'e | ||
| Theorem | jari 147* | Reverse inference form of df-ja 145 (Contributed by la korvo, 16-Aug-2023.) |
| ⊢ ga ko'a bu'a ko'e gi ko'a
bu'e ko'e ⊢ ko'a bu'a ja
bu'e ko'e | ||
| Syntax | tgiha 148 |
|
| brirebla bo'a gi'a bo'e | ||
| Definition | df-giha 149 | Definition of {gi'a} in terms of {ga}. |
| ⊢ go ko'a bo'a gi'a bo'e gi ga ko'a bo'a gi ko'a bo'e | ||
| Theorem | gihai 150 | Inference form of df-giha 149 (Contributed by la korvo, 14-Aug-2023.) |
| ⊢ ko'a bo'a
gi'a bo'e ⊢ ga ko'a bo'a gi
ko'a bo'e | ||
| Theorem | gihari 151 | Inference form of df-giha 149 (Contributed by la korvo, 14-Aug-2023.) |
| ⊢ ga ko'a bo'a gi
ko'a bo'e ⊢ ko'a bo'a
gi'a bo'e | ||
| Syntax | sjo 152 |
|
| sumti ko'a .o ko'e | ||
| Definition | df-o 153 | Definition of {.o} in terms of {go}. By analogy with forethought version of example 12.2-5 from [CLL] p. 14. |
| ⊢ go ko'a .o ko'e bo'a gi go ko'a bo'a gi ko'e bo'a | ||
| Theorem | oi 154 | Inference form of df-o 153 (Contributed by la korvo, 9-Aug-2023.) |
| ⊢ ko'a .o ko'e
bo'a ⊢
go ko'a bo'a gi ko'e
bo'a | ||
| Theorem | ori 155 | Reverse inference form of df-o 153 (Contributed by la korvo, 9-Aug-2023.) |
| ⊢ go ko'a bo'a gi
ko'e bo'a ⊢ ko'a .o ko'e
bo'a | ||
| Theorem | o-com 156 | {.o} commutes. (Contributed by la korvo, 14-Aug-2023.) |
| ⊢ go ko'a .o ko'e bo'a gi ko'e .o ko'a bo'a | ||
| Theorem | o-comi 157 | Inference form of o-com 156 (Contributed by la korvo, 16-Jul-2023.) |
| ⊢ ko'a .o ko'e
bo'a ⊢ ko'e .o ko'a
bo'a | ||
| Theorem | o-refl 158 | {.o} is reflexive over any brirebla. (Contributed by la korvo, 14-Aug-2024.) |
| ⊢ ko'a .o ko'a bo'a | ||
| Syntax | sbjo 159* |
|
| selbri bu'a jo bu'e | ||
| Definition | df-jo 160* | Definition of {jo} in terms of {go}. By analogy with example 12.2-5 of [CLL] p. 14. |
| ⊢ go ko'a bu'a jo bu'e ko'e gi go ko'a bu'a ko'e gi ko'a bu'e ko'e | ||
| Theorem | joi 161* | Inference form of df-jo 160 (Contributed by la korvo, 17-Jul-2023.) |
| ⊢ ko'a bu'a jo
bu'e ko'e ⊢ go
ko'a bu'a ko'e gi ko'a
bu'e ko'e | ||
| Theorem | jori 162* | Reverse inference form of df-jo 160 (Contributed by la korvo, 17-Jul-2023.) |
| ⊢ go ko'a bu'a ko'e gi ko'a
bu'e ko'e ⊢ ko'a bu'a jo
bu'e ko'e | ||
| Syntax | tgiho 163 |
|
| brirebla bo'a gi'o bo'e | ||
| Definition | df-giho 164 | Definition of {gi'o} in terms of {go}. |
| ⊢ go ko'a bo'a gi'o bo'e gi go ko'a bo'a gi ko'a bo'e | ||
| Theorem | gihoi 165 | Inference form of df-giho 164 (Contributed by la korvo, 14-Aug-2023.) |
| ⊢ ko'a bo'a
gi'o bo'e ⊢ go ko'a bo'a gi
ko'a bo'e | ||
| Theorem | gihori 166 | Inference form of df-giho 164 (Contributed by la korvo, 14-Aug-2023.) |
| ⊢ go ko'a bo'a gi
ko'a bo'e ⊢ ko'a bo'a
gi'o bo'e | ||
| Syntax | sbs 167 | If {bu'a} is a selbri, then so is {se bu'a}. |
| selbri se bu'a | ||
| Definition | df-se 168 | Definition of {se} as a swap of terbri. Implied by example 11.1-2 of [CLL] p. 5. |
| ⊢ go ko'e se bu'a ko'a gi ko'a bu'a ko'e | ||
| Theorem | sei 169 | From example 11.1-2 of [CLL] p. 5, where {mi prami do} and {do se prami mi} are equivalent. Inference form of df-se 168 (Contributed by la korvo, 17-Jul-2023.) |
| ⊢ ko'e se bu'a
ko'a ⊢ ko'a bu'a ko'e | ||
| Theorem | seri 170 | From example 11.1-2 of [CLL] p. 5, where {mi prami do} and {do se prami mi} are equivalent. Reverse inference form of df-se 168 (Contributed by la korvo, 17-Jul-2023.) |
| ⊢ ko'a bu'a ko'e ⊢ ko'e se bu'a
ko'a | ||
| Theorem | se-invo 171 | {se} is an involution. (Contributed by la korvo, 18-Jul-2023.) |
| ⊢ ko'a se se bu'a ko'e ⊢ ko'a bu'a ko'e | ||
| Theorem | se-dual 172* | Self-duality property for {se}. (Contributed by la korvo, 30-Jun-2024.) |
| ⊢ ko'a bu'a naja
bu'e ko'e ⊢ ko'e se bu'a
naja se bu'e ko'a | ||
| Theorem | se-dual-l 173* | Shift {se} to the left of an implication. (Contributed by la korvo, 30-Jun-2024.) |
| ⊢ ko'a bu'a naja
se bu'e ko'e ⊢ ko'e se bu'a
naja bu'e ko'a | ||
| Theorem | se-dual-r 174* | Shift {se} to the right of an implication. (Contributed by la korvo, 30-Jun-2024.) |
| ⊢ ko'a se bu'a
naja bu'e ko'e ⊢ ko'e bu'a naja
se bu'e ko'a | ||
| Theorem | se-ganaii 175* | Convert selbri on both sides of an implication simultaneously. (Contributed by la korvo, 19-Jul-2024.) |
| ⊢ ganai ko'a bu'a ko'e gi ko'i
bu'e ko'o ⊢ ganai
ko'e se bu'a ko'a gi
ko'o se bu'e ko'i | ||
| Theorem | se-ganair 176* | Convert selbri on both sides of an implication simultaneously. (Contributed by la korvo, 19-Jul-2024.) |
| ⊢ ganai ko'a se bu'a
ko'e gi ko'i se bu'e
ko'o ⊢ ganai
ko'e bu'a ko'a gi ko'o
bu'e ko'i | ||
| Syntax | brd 177 | Syntax for first-order universal quantification. |
| bridi broda bridi
ro da zo'u broda | ||
| Syntax | brb 178 | Syntax for second-order universal quantification. |
| bridi broda bridi
ro bu'a zo'u broda | ||
| Axiom | ax-gen1 179 | Axiom of first-order generalization. |
| ⊢ broda ⊢ ro
da zo'u broda | ||
| Axiom | ax-gen2 180 | Axiom of second-order generalization. |
| ⊢ broda ⊢ ro
bu'a zo'u broda | ||
| Axiom | ax-spec1 181 | Axiom of first-order specialization. Axiom ax-4 in [ILE] p. 0. |
| ⊢ ganai ro da zo'u broda gi broda | ||
| Theorem | spec1i 182 | Inference form of ax-spec1 181 Theorem spi in [ILE] p. 0. (Contributed by la korvo, 22-Jun-2024.) |
| ⊢ ro da zo'u broda ⊢ broda | ||
| Axiom | ax-spec2 183 | Axiom of second-order specialization, by analogy with ax-spec1 181 |
| ⊢ ganai ro bu'a zo'u broda gi broda | ||
| Theorem | spec2i 184 | Inference form of ax-spec2 183 (Contributed by la korvo, 23-Jun-2024.) |
| ⊢ ro bu'a zo'u broda ⊢ broda | ||
| Axiom | ax-qi1 185 | Axiom of quantified implication: if {ganai broda gi brode} under some universal quantifier, then the universal quantification of {broda} implies the universal quantification of {brode}. Relationally, the tuples of the consequent might not have the same data as the tuples of the antecedent; we only know that they exist, not that they are related. Axiom ax-5 in [ILE] p. 0. |
| ⊢ ganai ro da zo'u ganai broda gi brode gi ganai ro da zo'u broda gi ro da zo'u brode | ||
| Theorem | qi1i 186 | Inference form of ax-qi1 185 (Contributed by la korvo, 23-Jun-2024.) |
| ⊢ ro da zo'u ganai broda gi brode ⊢ ganai
ro da zo'u broda gi ro da zo'u brode | ||
| Theorem | qi1-mp 187 | Inference form of ax-qi1 185. Like ax-mp 10 under {ro da}. (Contributed by la korvo, 23-Jun-2024.) |
| ⊢ ro da zo'u ganai broda gi brode ⊢ ro
da zo'u broda ⊢ ro
da zo'u brode | ||
| Axiom | ax-qi2 188 | A variant of ax-qi1 185 for second-order quantifiers. Very few claims will be invariant under free choice of {bu'a}, but those that are should be subject to this transformation by analogy to first-order reasoning and an appeal to set theory. |
| ⊢ ganai ro bu'a zo'u ganai broda gi brode gi ganai ro bu'a zo'u broda gi ro bu'a zo'u brode | ||
| Theorem | qi2i 189 | Inference form of ax-qi2 188 (Contributed by la korvo, 23-Jun-2024.) |
| ⊢ ro bu'a zo'u ganai broda gi brode ⊢ ganai
ro bu'a zo'u broda gi ro bu'a zo'u brode | ||
| Theorem | qi2-mp 190 | Inference form of ax-qi2 188. Like ax-mp 10 under {ro bu'a}. (Contributed by la korvo, 23-Jun-2024.) |
| ⊢ ro bu'a zo'u ganai broda gi brode ⊢ ro
bu'a zo'u broda ⊢ ro
bu'a zo'u brode | ||
| Axiom | ax-ro-inst-2u 191 | {ro bu'a} may be instantiated with any selbri. As example 13.3 of [CLL] p. 16 notes, this will be of limited use, and is included largely to allow for a second-order definition of equality. |
| brirebla bo'a ⊢ ro
bu'e zo'u ko'a bu'e ⊢ ko'a bo'a | ||
| Axiom | ax-ro-inst-1u 192 | {ro da} may be instantiated with any sumti. |
| sumti ko'a ⊢ ro
da zo'u da bo'a ⊢ ko'a bo'a | ||
| Theorem | ro2-mp 193 | Modus ponens under {ro bu'a}. (Contributed by la korvo, 23-Jun-2024.) |
| ⊢ ro bu'a zo'u broda ⊢ ganai
broda gi brode ⊢ ro
bu'a zo'u brode | ||
| Theorem | ro2-bi 194 | Biconditional modus ponens under {ro bu'a}. (Contributed by la korvo, 16-Jul-2023.) |
| ⊢ ro bu'a zo'u broda ⊢ go
broda gi brode ⊢ ro
bu'a zo'u brode | ||
| Theorem | ro2-bi-rev 195 | Biconditional modus ponens under {ro bu'a}. (Contributed by la korvo, 16-Aug-2023.) |
| ⊢ ro bu'a zo'u broda ⊢ go
brode gi broda ⊢ ro
bu'a zo'u brode | ||
| Syntax | sbdu 196 | Identity as a binary relation. |
| selbri du | ||
| Definition | df-du 197 | A second-order characterization of identity which is non-first-order-izable. |
| ⊢ go ko'a du ko'e gi ro bu'a zo'u ko'a .o ko'e bu'a | ||
| Theorem | dui 198 | Inference form of df-du 197 (Contributed by la korvo, 18-Jul-2023.) |
| ⊢ ko'a du ko'e ⊢ ro
bu'a zo'u ko'a .o ko'e
bu'a | ||
| Theorem | duis 199 | Sugared inference form of df-du 197 (Contributed by la korvo, 23-Jun-2024.) |
| ⊢ ko'a du ko'e ⊢ go
ko'a bu'a
gi ko'e bu'a | ||
| Theorem | duri 200 | Reverse inference form of df-du 197 (Contributed by la korvo, 18-Jul-2023.) |
| ⊢ ro bu'a zo'u ko'a
.o ko'e bu'a ⊢ ko'a du ko'e | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |