HomeTheorem List (p. 2 of 10)
Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List
| Home |
brismu
bridi Theorem List (p. 2 of 10) |
< Previous Next >
|
|
Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List | ||
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | najaii 101* | Inference form of df-naja 99 (Contributed by la korvo, 17-Aug-2023.) |
⊢ ko'a bu'a naja
bu'e ko'e  ⊢ ko'a bu'a ko'e  ⊢ ko'a bu'e ko'e | ||
| Theorem | najari 102* | Reverse inference form of df-naja 99 (Contributed by la korvo, 17-Aug-2023.) |
| ⊢ ganai ko'a bu'a ko'e gi ko'a
bu'e ko'e ⊢ ko'a bu'a naja
bu'e ko'e | ||
| Definition | df-naja-t 103* | Extension of df-naja 99 to ternary bridi. |
| ⊢ go ko'a bu'a naja bu'e ko'e ko'i gi ganai ko'a bu'a ko'e ko'i gi ko'a bu'e ko'e ko'i | ||
| Syntax | sbjanai 104* |
|
| selbri bu'a janai bu'e | ||
| Definition | df-janai 105* | Definition of {janai} in terms of {ganai}. By analogy with example 12.2-5 of [CLL] p. 14. |
| ⊢ go ko'a bu'e janai bu'a ko'e gi ganai ko'a bu'a ko'e gi ko'a bu'e ko'e | ||
| Theorem | janaii 106* | Inference form of df-janai 105 (Contributed by la korvo, 16-Aug-2023.) |
| ⊢ ko'a bu'e
janai bu'a ko'e ⊢ ganai
ko'a bu'a ko'e gi ko'a
bu'e ko'e | ||
| Theorem | janaiii 107* | Inference form of df-janai 105 (Contributed by la korvo, 16-Aug-2023.) |
| ⊢ ko'a bu'e
janai bu'a ko'e ⊢ ko'a bu'a ko'e ⊢ ko'a bu'e ko'e | ||
| Theorem | janairi 108* | Reverse inference form of df-janai 105 (Contributed by la korvo, 16-Aug-2023.) |
| ⊢ ganai ko'a bu'a ko'e gi ko'a
bu'e ko'e ⊢ ko'a bu'e
janai bu'a ko'e | ||
| Syntax | tnagiha 109 |
|
| brirebla bo'a nagi'a bo'e | ||
| Definition | df-nagiha 110 | Definition of {nagi'a} in terms of {ganai}. |
| ⊢ go ko'a bo'a nagi'a bo'e gi ganai ko'a bo'a gi ko'a bo'e | ||
| Theorem | nagihai 111 | Inference form of df-nagiha 110 (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 112 | Inference form of df-nagiha 110 (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 113 | Inference form of df-nagiha 110 (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 114 |
|
| brirebla bo'a gi'anai bo'e | ||
| Definition | df-gihanai 115 | 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 116 | Inference form of df-gihanai 115 (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 117 | Inference form of df-gihanai 115 (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 118 | Inference form of df-gihanai 115 (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 119 | Lemma for ge-com 120 showing that {ge} is commutative in one direction. (Contributed by la korvo, 31-Jul-2023.) [Auxiliary lemma - not displayed.] |
| Theorem | ge-com 120 | {ge} is commutative. (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ go ge broda gi brode gi ge brode gi broda | ||
| Theorem | ge-go 121 | Conjunction implies biimplication. (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ ge broda gi brode ⊢ go
broda gi brode | ||
| Theorem | ge-diag 122 | {ge} admits the diagonal morphism. (Contributed by la korvo, 21-Aug-2024.) |
| ⊢ ganai broda gi ge broda gi broda | ||
| Theorem | ge-idem 123 | {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 124 |
|
| sumti ko'a .e ko'e | ||
| Definition | df-e 125 | 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 126 | Inference form of df-e 125 (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 127 | Reverse inference form of df-e 125 (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 128* |
|
| selbri bu'a je bu'e | ||
| Definition | df-je 129* | 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 130* | Inference form of df-je 129 (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 131* | Reverse inference form of df-je 129 (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 132 |
|
| brirebla bo'a gi'e bo'e | ||
| Definition | df-gihe 133 | 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 134 | Inference form of df-gihe 133 (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 135 | Inference form of df-gihe 133 (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 136 | Inference form of df-gihe 133 (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 137 |
|
| bridi ga broda gi brode | ||
| Definition | df-ga 138 | Definition of {ga} in terms of {go}, {ganai}, and {ge}. |
| ⊢ go ganai ga brode gi brodi gi broda gi ge ganai brode gi broda gi ganai brodi gi broda | ||
| Theorem | gai 139 | Inference form of df-ga 138 (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 140 | Reverse implication of df-ga 138 (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 141 | Reverse inference form of df-ga 138 (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 142 | Introduce {ga} with the antecedent on the left. (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ ganai broda gi ga broda gi brode | ||
| Theorem | ga-rin 143 | Introduce {ga} with the antecedent on the right. (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ ganai broda gi ga brode gi broda | ||
| Theorem | garii 144 | Nested inference form of gar 140 (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 145 | {ga} is idempotent. (Contributed by la korvo, 15-Aug-2024.) |
| ⊢ go ga broda gi broda gi broda | ||
| Theorem | ga-com-lem 146 | Lemma for ga-com 147 (Contributed by la korvo, 31-Jul-2023.) [Auxiliary lemma - not displayed.] |
| Theorem | ga-com 147 | {ga} commutes. (Contributed by la korvo, 31-Jul-2023.) |
| ⊢ go ga broda gi brode gi ga brode gi broda | ||
| Theorem | ga-li 148 | Deduce a disjunction on the left. (Contributed by la korvo, 4-Jan-2025.) |
| ⊢ broda ⊢ ga
broda gi brode | ||
| Theorem | ga-ri 149 | Deduce a disjunction on the right. (Contributed by la korvo, 4-Jan-2025.) |
| ⊢ broda ⊢ ga
brode gi broda | ||
| Theorem | ga-lid 150 | Deduction form of ga-li 148 (Contributed by la korvo, 4-Jan-2025.) |
| ⊢ ganai broda gi brode ⊢ ganai
broda gi ga brode gi brodi | ||
| Theorem | ga-rid 151 | Deduction form of ga-ri 149 (Contributed by la korvo, 4-Jan-2025.) |
| ⊢ ganai broda gi brode ⊢ ganai
broda gi ga brodi gi brode | ||
| Syntax | sja 152 |
|
| sumti ko'a .a ko'e | ||
| Definition | df-a 153 | 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 154 | Inference form of df-a 153 (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 155 | Inference form of df-a 153 (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 156 | {.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 157 | Inference form of a-com 156 |
| ⊢ ko'a .a ko'e
bo'a ⊢ ko'e .a ko'a
bo'a | ||
| Syntax | sbja 158* |
|
| selbri bu'a ja bu'e | ||
| Definition | df-ja 159* | 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 160* | Inference form of df-ja 159 (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 161* | Reverse inference form of df-ja 159 (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 162 |
|
| brirebla bo'a gi'a bo'e | ||
| Definition | df-giha 163 | 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 164 | Inference form of df-giha 163 (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 165 | Inference form of df-giha 163 (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 166 |
|
| sumti ko'a .o ko'e | ||
| Definition | df-o 167 | 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 168 | Inference form of df-o 167 (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 169 | Reverse inference form of df-o 167 (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 170 | {.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 171 | Inference form of o-com 170 (Contributed by la korvo, 16-Jul-2023.) |
| ⊢ ko'a .o ko'e
bo'a ⊢ ko'e .o ko'a
bo'a | ||
| Theorem | o-refl 172 | {.o} is reflexive over any brirebla. (Contributed by la korvo, 14-Aug-2024.) |
| ⊢ ko'a .o ko'a bo'a | ||
| Syntax | sbjo 173* |
|
| selbri bu'a jo bu'e | ||
| Definition | df-jo 174* | 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 175* | Inference form of df-jo 174 (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 176* | Reverse inference form of df-jo 174 (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 177 |
|
| brirebla bo'a gi'o bo'e | ||
| Definition | df-giho 178 | 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 179 | Inference form of df-giho 178 (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 180 | Inference form of df-giho 178 (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 181 | If {bu'a} is a selbri, then so is {se bu'a}. |
| selbri se bu'a | ||
| Definition | df-se 182 | 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 183 | 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 182 (Contributed by la korvo, 17-Jul-2023.) |
| ⊢ ko'e se bu'a
ko'a ⊢ ko'a bu'a ko'e | ||
| Theorem | seri 184 | 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 182 (Contributed by la korvo, 17-Jul-2023.) |
| ⊢ ko'a bu'a ko'e ⊢ ko'e se bu'a
ko'a | ||
| Theorem | se-invo 185 | {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 186* | 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 187* | 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 188* | 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 189* | 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 190* | 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 191 | Syntax for first-order universal quantification. |
| bridi broda bridi ro da
zo'u broda | ||
| Syntax | brb 192 | Syntax for second-order universal quantification. |
| bridi broda bridi ro bu'a
zo'u broda | ||
| Axiom | ax-gen1 193 | Axiom of first-order generalization. |
| ⊢ broda ⊢ ro
da zo'u broda | ||
| Theorem | mpg1 194 | Modus ponens with generalization. (Contributed by la korvo, 3-Jan-2025.) |
| ⊢ ganai
ro da zo'u broda gi brode ⊢ broda ⊢ brode | ||
| Axiom | ax-gen2 195 | Axiom of second-order generalization. |
| ⊢ broda ⊢ ro
bu'a zo'u broda | ||
| Axiom | ax-spec1 196 | Axiom of first-order specialization. |
| ⊢ ganai ro da zo'u broda gi broda | ||
| Theorem | spec1i 197 | Inference form of ax-spec1 196 (Contributed by la korvo, 22-Jun-2024.) |
| ⊢ ro da zo'u broda ⊢ broda | ||
| Theorem | spec1d 198 | Deduction form of ax-spec1 196 (Contributed by la korvo, 4-Jan-2025.) |
| ⊢ ganai broda gi ro da zo'u brode ⊢ ganai
broda gi brode | ||
| Axiom | ax-spec2 199 | Axiom of second-order specialization, by analogy with ax-spec1 196 |
| ⊢ ganai ro bu'a zo'u broda gi broda | ||
| Theorem | spec2i 200 | Inference form of ax-spec2 199 (Contributed by la korvo, 23-Jun-2024.) |
| ⊢ ro bu'a zo'u broda ⊢ broda | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |