HomeHome brismu bridi
Theorem List (p. 3 of 11)
< Previous  Next >

Mirrors  >  Metamath Home Page  >  Home Page  >  Theorem List Contents       This page: Page List

Theorem List for brismu bridi - 201-300   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremo-com 201 {.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
 
Theoremo-comi 202 Inference form of o-com 201 (Contributed by la korvo, 16-Jul-2023.)
ko'a .o ko'e bo'a   =>   ⊢ ko'e .o ko'a bo'a
 
Theoremo-refl 203 {.o} is reflexive over any brirebla. (Contributed by la korvo, 14-Aug-2024.)
ko'a .o ko'a bo'a
 
1.8.2  {jo}
 
Syntaxsbjo 204*

selbri bu'a jo bu'e
 
Definitiondf-jo 205* 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
 
Theoremjoi 206* Inference form of df-jo 205 (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
 
Theoremjori 207* Reverse inference form of df-jo 205 (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
 
1.8.3  {gi'o}
 
Syntaxtgiho 208

brirebla bo'a gi'o bo'e
 
Definitiondf-giho 209 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
 
Theoremgihoi 210 Inference form of df-giho 209 (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
 
Theoremgihori 211 Inference form of df-giho 209 (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
 
1.9  Conversion I: {se}
 
Syntaxsbs 212 If {bu'a} is a selbri, then so is {se bu'a}.
selbri se bu'a
 
Definitiondf-se 213 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
 
Theoremsei 214 From example 11.1-2 of [CLL] p. 5, where {mipramido} and {do se pramimi} are equivalent. Inference form of df-se 213 (Contributed by la korvo, 17-Jul-2023.)
ko'e se bu'a ko'a   =>   ⊢ ko'a bu'a ko'e
 
Theoremseri 215 From example 11.1-2 of [CLL] p. 5, where {mipramido} and {do se pramimi} are equivalent. Reverse inference form of df-se 213 (Contributed by la korvo, 17-Jul-2023.)
ko'a bu'a ko'e   =>   ⊢ ko'e se bu'a ko'a
 
Theoremse-invo 216 {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
 
Theoremse-dual 217* 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
 
Theoremse-dual-l 218* 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
 
Theoremse-dual-r 219* 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
 
Theoremse-ganaii 220* 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
 
Theoremse-ganair 221* 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
 
1.10  Universal quantifiers I: {ro}
 
Syntaxbrd 222 Syntax for first-order universal quantification.
bridi ro da zo'u broda
 
Syntaxbrb 223 Syntax for second-order universal quantification.
bridi ro bu'a zo'u broda
 
Axiomax-gen1 224 Axiom of first-order generalization.
broda   =>   ⊢ ro da zo'u broda
 
Theoremmpg1 225 Modus ponens with generalization. (Contributed by la korvo, 3-Jan-2025.)
ganai ro da zo'u broda gi brode   &   ⊢ broda   =>   ⊢ brode
 
Theorembig1 226 Modus ponens with generalization. (Contributed by la korvo, 9-Jul-2025.)
go ro da zo'u broda gi brode   &   ⊢ broda   =>   ⊢ brode
 
Axiomax-gen2 227 Axiom of second-order generalization.
broda   =>   ⊢ ro bu'a zo'u broda
 
Axiomax-spec1 228 Axiom of first-order specialization.
ganai ro da zo'u broda gi broda
 
Theoremspec1i 229 Inference form of ax-spec1 228 (Contributed by la korvo, 22-Jun-2024.)
ro da zo'u broda   =>   ⊢ broda
 
Theoremspec1d 230 Deduction form of ax-spec1 228 (Contributed by la korvo, 4-Jan-2025.)
ganai broda gi ro da zo'u brode   =>   ⊢ ganai broda gi brode
 
Theoremspec1s 231 Generalize an antecedent. (Contributed by la korvo, 8-Jul-2025.)
ganai broda gi brode   =>   ⊢ ganai ro da zo'u broda gi brode
 
Axiomax-spec2 232 Axiom of second-order specialization, by analogy with ax-spec1 228
ganai ro bu'a zo'u broda gi broda
 
Theoremspec2i 233 Inference form of ax-spec2 232 (Contributed by la korvo, 23-Jun-2024.)
ro bu'a zo'u broda   =>   ⊢ broda
 
Axiomax-qi1 234 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.
ganai ro da zo'u ganai broda gi brode gi ganai ro da zo'u broda gi ro da zo'u brode
 
Theoremqi1i 235 Inference form of ax-qi1 234 (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
 
Theoremqi1-mp 236 Inference form of ax-qi1 234. 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
 
Theoremqi1q 237 Quantify over both sides of an implication. (Contributed by la korvo, 8-Jul-2025.)
ganai broda gi brode   =>   ⊢ ganai ro da zo'u broda gi ro da zo'u brode
 
Theoremalrimih 238 An inference. (Contributed by la korvo, 9-Jul-2025.)
ganai broda gi ro da zo'u broda   &   ⊢ ganai broda gi brode   =>   ⊢ ganai broda gi ro da zo'u brode
 
Axiomax-qi2 239 A variant of ax-qi1 234 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
 
Theoremqi2i 240 Inference form of ax-qi2 239 (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
 
Theoremqi2-mp 241 Inference form of ax-qi2 239. 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
 
Axiomax-ro-inst-2u 242 {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
 
Axiomax-ro-inst-1u 243 {ro da} may be instantiated with any sumti.
sumti ko'a   &   ⊢ ro da zo'u da bo'a   =>   ⊢ ko'a bo'a
 
Theoremro2-mp 244 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
 
Theoremro2-bi 245 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
 
Theoremro2-bi-rev 246 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
 
Axiomax-ro1-com 247* First-order universal quantifiers commute.
ganai ro da zo'u ro de zo'u broda gi ro de zo'u ro da zo'u broda
 
Theoremro1-coms 248* Swap quantifiers on the antecedent. (Contributed by la korvo, 4-Jan-2025.)
ganai ro da zo'u ro de zo'u broda gi brode   =>   ⊢ ganai ro de zo'u ro da zo'u broda gi brode
 
Axiomax-ro1-nf 249 First-order universal quantifiers bind their variables.
ganai ro da zo'u broda gi ro da zo'u ro da zo'u broda
 
1.11  Identity: {du}
 
Syntaxsbdu 250 Identity as a binary relation.
selbri du
 
Definitiondf-du 251 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
 
Theoremdui 252 Inference form of df-du 251 (Contributed by la korvo, 18-Jul-2023.)
ko'a du ko'e   =>   ⊢ ro bu'a zo'u ko'a .o ko'e bu'a
 
Theoremduis 253 Sugared inference form of df-du 251 (Contributed by la korvo, 23-Jun-2024.)
ko'a du ko'e   =>   ⊢ go ko'a bu'a gi ko'e bu'a
 
Theoremduri 254 Reverse inference form of df-du 251 (Contributed by la korvo, 18-Jul-2023.)
ro bu'a zo'u ko'a .o ko'e bu'a   =>   ⊢ ko'a du ko'e
 
Theoremduris 255 Sugared reverse inference form of df-du 251 (Contributed by la korvo, 23-Jun-2024.)
go ko'a bu'a gi ko'e bu'a   =>   ⊢ ko'a du ko'e
 
Theoremdu-refl 256 {du} is reflexive. (Contributed by la korvo, 16-Aug-2023.) (Shortened by la korvo, 23-Jun-2024.)
ko'a du ko'a
 
Theoremdu-trans 257 {du} is transitive. (Contributed by la korvo, 16-Aug-2023.) (Shortened by la korvo, 23-Jun-2024.)
ko'a du ko'e   &   ⊢ ko'e du ko'i   =>   ⊢ ko'a du ko'i
 
Axiomax-du-trans 258 A not-quite-transitive law of equality.
ganai ko'a du ko'e gi ganai ko'a du ko'i gi ko'e du ko'i
 
Theoremdu-symi 259 {du} is symmetric. (Contributed by la korvo, 16-Aug-2023.) (Shortened by la korvo, 23-Jun-2024.)
ko'a du ko'e   =>   ⊢ ko'e du ko'a
 
Theoremdu-sym-ganai 260 An internal version of du-symi 259 (Contributed by la korvo, 4-Jan-2025.)
ganai ko'a du ko'e gi ko'e du ko'a
 
Theoremdu-sym-go 261 An internal version of du-symi 259 (Contributed by la korvo, 4-Jan-2025.)
go ko'a du ko'e gi ko'e du ko'a
 
Theoremse-du-elim 262 {se du} may be replaced with {du}. Theorem Cat.Allegory.Base.dual-id in [1Lab] p. 0. (Contributed by la korvo, 9-Jul-2023.)
ko'a se du ko'e   =>   ⊢ ko'a du ko'e
 
Axiomax-vsub 263* An axiom of variable substitution.
ganai da du de gi ganai ro de zo'u broda gi ro da zo'u ganai da du de gi broda
 
Axiomax-ro1-sub 264* First-order quantifier substitution.
ganai ro da zo'u da du de gi ro de zo'u de du da
 
Axiomax-ro-int 265* First-order universal quantifier introduction with a scope gadget.
ga ro di zo'u di du da gi ga ro di zo'u di du de gi ro di zo'u ganai da du de gi ro di zo'u da du de
 
1.12  Boolean predicates: {cei'i}
 
Syntaxbceihi 266

bridi cei'i
 
Definitiondf-ceihi 267 The predicate which is always true. Note that both sides are relational: the left-hand side definitionally only has one inhabitant, so this definition asserts that {ko'a du ko'a} is only true via one path. For related statements which reinforce this idea, see ceihi 268 or ceihi-nf 443.
go cei'i gi ko'a du ko'a
 
Theoremceihi 268 {cei'i} is always true. (Contributed by la korvo, 18-Jul-2023.)
cei'i
 
Theoremmp-ceihi 269 A proposition implied by {cei'i} is always true. (Contributed by la korvo, 4-Jan-2025.)
ganai cei'i gi broda   =>   ⊢ broda
 
Theoremceihi-term 270 {cei'i} is the terminal object. (Contributed by la korvo, 4-Jan-2025.)
ganai broda gi cei'i
 
1.13  Negation I: {gai'o}, {naku}

Lojban classically contains a {na} which may slide around in a prenex and between connectives. To be constructive, we will more carefully introduce {naku} negation within the prenex first, and then justify various simplifications and rearrangements.

 
Syntaxbgaiho 271

bridi gai'o
 
Syntaxbnk 272 Syntax for negation over an empty row of quantifiers.
bridi naku broda
 
Definitiondf-naku 273 Traditional definition of intuitionistic negation.
go naku broda gi ganai broda gi gai'o
 
Theoremnaku-uncur 274 Uncurried form of df-naku 273 (Contributed by la korvo, 20-Aug-2023.)
ganai ge naku broda gi broda gi gai'o
 
Theoremlnc 275 The law of non-contradiction. No bridi is simultaneously inhabited and uninhabited. (Contributed by la korvo, 19-Sep-2024.)
naku ge naku broda gi broda
 
Theoremlnci 276 The law of non-contradiction. If a bridi is simultaneously inhabited and uninhabited, then we reach an absurdity. (Contributed by la korvo, 20-Aug-2023.)
ge broda gi naku broda   =>   ⊢ gai'o
 
Theoremnakui 277 Inference form of df-naku 273 (Contributed by la korvo, 9-Aug-2023.)
naku broda   =>   ⊢ ganai broda gi gai'o
 
Theoremnakuii 278 Inference form of df-naku 273 (Contributed by la korvo, 9-Aug-2023.)
naku broda   &   ⊢ broda   =>   ⊢ gai'o
 
Theoremnakuri 279 Reverse inference form of df-naku 273 (Contributed by la korvo, 9-Aug-2023.)
ganai broda gi gai'o   =>   ⊢ naku broda
 
Theoremna-gaiho 280 {gai'o} is uninhabited. (Contributed by la korvo, 9-Aug-2023.)
naku gai'o
 
Axiomax-sdo 281 The principle of self-defeating objects. If an object's existence would imply that it doesn't exist -- usually via contradiction -- then it doesn't exist. As a special case, if some tuple's membership in a relation would imply non-membership in that relation, then it's not a member. For a survey of this principle across maths, see [Tao].
ganai ganai broda gi naku broda gi naku broda
 
Theoremsdoi 282 Inference form of ax-sdo 281 (Contributed by la korvo, 9-Aug-2023.)
ganai broda gi naku broda   =>   ⊢ naku broda
 
Theoremsdod 283 Deduction form of ax-sdo 281 (Contributed by la korvo, 4-Jan-2025.)
ganai broda gi ganai brode gi naku brode   =>   ⊢ ganai broda gi naku brode
 
Axiomax-efq 284 The principle of explosion. If a tuple both is and is not a member of some relation, then we are inconsistent and any theorem whatsoever may be derived. The short name "efq" comes from the Latin phrase, "ex falso quodlibet".
ganai naku broda gi ganai broda gi brode
 
Theoremefqi 285 Inference form of ax-efq 284 (Contributed by la korvo, 25-Jun-2024.)
naku broda   =>   ⊢ ganai broda gi brode
 
Theoremefqd 286 Deduction form of ax-efq 284 (Contributed by la korvo, 4-Jan-2025.)
ganai broda gi naku brode   =>   ⊢ ganai broda gi ganai brode gi brodi
 
Theoremefqii 287 Inference form of ax-efq 284 (Contributed by la korvo, 25-Jun-2024.)
naku broda   &   ⊢ broda   =>   ⊢ brode
 
Theoremgaiho-init 288 From falsity, anything is possible. (Contributed by la korvo, 14-Jul-2025.)
ganai gai'o gi broda
 
Theoremcon2d 289 A contrapositive deduction. (Contributed by la korvo, 1-Jan-2025.)
ganai broda gi ganai brode gi naku brodi   =>   ⊢ ganai broda gi ganai brodi gi naku brode
 
Theoremmt2d 290 Deduction form of modus tollens. (Contributed by la korvo, 1-Jan-2025.)
ganai broda gi brode   &   ⊢ ganai broda gi ganai brodi gi naku brode   =>   ⊢ ganai broda gi naku brodi
 
Theoremnsyl3 291 A negated syllogism. Can be seen as a deduction form of modus tollens. (Contributed by la korvo, 1-Jan-2025.)
ganai broda gi naku brode   &   ⊢ ganai brodi gi brode   =>   ⊢ ganai brodi gi naku broda
 
Theoremcon2i 292 The standard contrapositive inference. (Contributed by la korvo, 1-Jan-2025.)
ganai broda gi naku brode   =>   ⊢ ganai brode gi naku broda
 
Theoremnakunaku 293 Double negation is a functor. (Contributed by la korvo, 4-Jan-2025.)
ganai broda gi naku naku broda
 
Theoremnakunakui 294 Inference form of nakunaku 293 (Contributed by la korvo, 4-Jan-2025.)
broda   =>   ⊢ naku naku broda
 
Theoremnsyl 295 A negated syllogism. Can be seen as a deduction form of modus tollens. (Contributed by la korvo, 1-Jan-2025.)
ganai broda gi naku brode   &   ⊢ ganai brodi gi brode   =>   ⊢ ganai broda gi naku brodi
 
Theoremstewart 296 A syllogism underlying the Swallowing Elephants puzzle from chapter 4 of [Stewart] p. 22. (Contributed by la korvo, 1-Jan-2025.)
ganai broda gi brode   &   ⊢ ganai brodi gi brodo   &   ⊢ ganai brodu gi brodi   &   ⊢ ganai brode gi naku brodo   =>   ⊢ ganai broda gi naku brodu
 
1.14  Mutual exclusion I

The final of our five essential connectives. As with disjunctions, we can introduce all versions of mutual exclusion at once.

 
1.14.1  {gonai}
 
Syntaxbgon 297

bridi gonai broda gi brode
 
Definitiondf-gonai 298 Standard constructive definition of mutual exclusion ("the exclusive OR"), based on the mnemonic given to computer scientists in the USA and UK: "It's cake or tea, but not cake and tea."
go gonai broda gi brode gi ge ga broda gi brode gi naku ge broda gi brode
 
Theoremgonaii 299 Inference form of df-gonai 298 (Contributed by la korvo, 8-Aug-2023.)
gonai broda gi brode   =>   ⊢ ge ga broda gi brode gi naku ge broda gi brode
 
Theoremgonaiil 300 Inference form of df-gonai 298 (Contributed by la korvo, 8-Aug-2023.)
gonai broda gi brode   =>   ⊢ ga broda gi brode
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1048
  Copyright terms: Public domain < Previous  Next >