HomeTheorem List (p. 4 of 10)
Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List
| Home |
brismu
bridi Theorem List (p. 4 of 10) |
< Previous Next >
|
|
Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List | ||
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | gripau-refl 301 | {gripau} is reflexive. (Contributed by la korvo, 15-Jul-2024.) |
| ⊢ ko'a gripau ko'a | ||
| Theorem | gripau-trans 302 | {gripau} is transitive. (Contributed by la korvo, 19-Jul-2024.) |
⊢ ko'a gripau ko'e  ⊢ ko'e gripau ko'i  ⊢ ko'a gripau ko'i | ||
The internal hom is the syntax which internalizes relations. We define {ka} abstractions as well as several useful gismu for accessing the contents of those abstractions. Our approach uses {1 ka} quantification in acknowledgement of isomorphism-invariance. | ||
| Syntax | sc 303 |
|
| sumti ce'u | ||
| Syntax | spk 304 | If {bo'a} is a brirebla, then filling its first place with a sumti and wrapping it with {1 ka} yields sumti. |
| sumti 1 ka ko'a bo'a kei | ||
| Syntax | sbckaji 305 |
|
| selbri ckaji | ||
| Theorem | bckaji 306 | {ckaji} is often found with this conjugation. (Contributed by la korvo, 14-Aug-2023.) |
| bridi ko'a ckaji 1 ka ce'u bo'a kei | ||
| Definition | df-ckaji 307 | Definition of {ckaji} from {ka}. Based on example 4.1-2 of [CLL] p. 11. |
| ⊢ go ko'a ckaji 1 ka ce'u bo'a kei gi ko'a bo'a | ||
| Theorem | ckajii 308 | Inference form of df-ckaji 307 (Contributed by la korvo, 17-Jul-2023.) |
| ⊢ ko'a ckaji 1 ka ce'u bo'a kei ⊢ ko'a bo'a | ||
| Theorem | ckajiri 309 | Reverse inference form of df-ckaji 307 (Contributed by la korvo, 17-Jul-2023.) |
| ⊢ ko'a bo'a ⊢ ko'a ckaji 1 ka ce'u bo'a kei | ||
| Syntax | sbckini 310 |
|
| selbri ckini | ||
| Theorem | bckini 311 | {ckini} is often found with this conjugation. (Contributed by la korvo, 14-Aug-2023.) |
| bridi ko'a ckini ko'e 1 ka ce'u bu'a ce'u kei | ||
| Definition | df-ckini 312 |
|
| ⊢ go ko'a ckini ko'e 1 ka ce'u bu'a ce'u kei gi ko'a bu'a ko'e | ||
| Theorem | ckinii 313 | Inference form of df-ckini 312 (Contributed by la korvo, 17-Jul-2023.) |
| ⊢ ko'a ckini ko'e 1 ka
ce'u bu'a ce'u
kei ⊢ ko'a bu'a ko'e | ||
| Theorem | ckiniri 314 | Reverse inference form of df-ckini 312 (Contributed by la korvo, 17-Jul-2023.) |
| ⊢ ko'a bu'a ko'e ⊢ ko'a ckini ko'e 1 ka
ce'u bu'a ce'u
kei | ||
| Theorem | ckini-se 315 | {se} can be inserted underneath ckini3. Example theorem from early draft of la brismu. (Contributed by la korvo, 12-Jul-2023.) |
| ⊢ ko'a ckini ko'e 1 ka
ce'u bu'a ce'u
kei ⊢ ko'e ckini ko'a 1 ka
ce'u se bu'a
ce'u kei | ||
| Syntax | sbsefsi 316 |
|
| selbri sefsi | ||
| Definition | df-sefsi 317 | A useful experimental gismu like {ckini}. In particular, {sefsi} can adapt between unary and binary {ka} abstractions. This definition was given by la xorxes. |
| ⊢ go ko'a sefsi ko'e gi ko'a ckini ko'a ko'e | ||
| Syntax | sbsimsa 318 |
|
| selbri simsa | ||
| Theorem | bsimsa 319 | {simsa} is often found with this conjugation. (Contributed by la korvo, 6-Aug-2023.) |
| bridi ko'a simsa ko'e 1 ka ce'u bu'a kei | ||
| Definition | df-simsa 320 | Definition of {simsa} in terms of {ckaji}. |
| ⊢ go ko'a simsa ko'e ko'i gi ko'a .e ko'e ckaji ko'i | ||
| Theorem | simsai 321 | Inference form of df-simsa 320 (Contributed by la korvo, 6-Aug-2023.) |
| ⊢ ko'a simsa ko'e ko'i ⊢ ko'a .e ko'e
ckaji ko'i | ||
| Theorem | simsail 322 | Inference form of df-simsa 320 (Contributed by la korvo, 6-Aug-2023.) |
| ⊢ ko'a simsa ko'e ko'i ⊢ ko'a ckaji ko'i | ||
| Theorem | simsair 323 | Inference form of df-simsa 320 (Contributed by la korvo, 6-Aug-2023.) |
| ⊢ ko'a simsa ko'e ko'i ⊢ ko'e ckaji ko'i | ||
| Theorem | simsari 324 | Reverse inference form of df-simsa 320 (Contributed by la korvo, 6-Aug-2023.) |
| ⊢ ko'a .e ko'e
ckaji ko'i ⊢ ko'a simsa ko'e ko'i | ||
| Theorem | simsarii 325 | Reverse inference form of df-simsa 320 (Contributed by la korvo, 6-Aug-2023.) |
| ⊢ ko'a ckaji ko'i ⊢ ko'e ckaji ko'i ⊢ ko'a simsa ko'e ko'i | ||
| Axiom | ax-simsa-sym 326 | {simsa} is symmetric. |
| ⊢ go ko'a simsa ko'e ko'i gi ko'e simsa ko'a ko'i | ||
| Syntax | sbdunli 327 |
|
| selbri dunli | ||
| Theorem | bdunli 328 | {dunli} is often found with this conjugation. (Contributed by la korvo, 23-Jun-2024.) |
| bridi ko'a dunli ko'e 1 ka ce'u bu'a ce'u kei | ||
| Definition | df-dunli 329 | Definition of {dunli} by la ilmen in terms of {ckini}. A metavariable is used instead of a universal quantifier to ease manipulation. |
| ⊢ go ko'a dunli ko'e ko'i gi ko'a .o ko'e ckini ko'o ko'i | ||
| Theorem | dunlii 330 | Inference form of df-dunli 329 (Contributed by la korvo, 23-Jun-2024.) |
| ⊢ ko'a dunli ko'e ko'i ⊢ ko'a .o ko'e
ckini ko'o ko'i | ||
| Theorem | dunliri 331 | Reverse inference form of df-dunli 329 (Contributed by la korvo, 23-Jun-2024.) |
| ⊢ ko'a .o ko'e
ckini ko'o ko'i ⊢ ko'a dunli ko'e ko'i | ||
| Theorem | dunli-refl 332 | {dunli} is reflexive over any dunli3. (Contributed by la korvo, 14-Aug-2024.) |
| ⊢ ko'a dunli ko'a ko'e | ||
| Theorem | dunli-sym 333 | Because modal x1 and modal x2 of {dunli} are definitionally interchangeable, {dunli} itself is symmetric. (Contributed by la korvo, 20-Sep-2024.) |
| ⊢ go ko'a dunli ko'e ko'i gi ko'e dunli ko'a ko'i | ||
| Syntax | sbmintu 334 |
|
| selbri mintu | ||
| Theorem | bmintu 335 | {mintu} is often found with this conjugation. (Contributed by la korvo, 6-Aug-2023.) |
| bridi ko'a mintu ko'e 1 ka ce'u bu'a kei | ||
| Definition | df-mintu 336 | Definition of {mintu} in terms of {ckaji}. |
| ⊢ go ko'a mintu ko'e ko'i gi ko'a .o ko'e ckaji ko'i | ||
| Theorem | mintui 337 | Inference form of df-mintu 336 (Contributed by la korvo, 6-Aug-2023.) |
| ⊢ ko'a mintu ko'e ko'i ⊢ ko'a .o ko'e
ckaji ko'i | ||
| Theorem | minturi 338 | Reverse inference form of df-mintu 336 (Contributed by la korvo, 6-Aug-2023.) |
| ⊢ ko'a .o ko'e
ckaji ko'i ⊢ ko'a mintu ko'e ko'i | ||
| Theorem | mintu-refl 339 | {mintu} is reflexive over any mintu3. (Contributed by la korvo, 14-Aug-2024.) |
| ⊢ ko'a mintu ko'a ko'e | ||
| Theorem | mintu-sym 340 | Because x1 and x2 of {mintu} are definitionally interchangeable, it is symmetric. (Contributed by la korvo, 20-Sep-2024.) |
| ⊢ go ko'a mintu ko'e ko'i gi ko'e mintu ko'a ko'i | ||
| Theorem | du-mintu 341 | Suggested by baseline definition of {mintu}: {du} is {mintu} without a standard of comparison, which is a stronger condition. (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ ko'a du ko'e ⊢ ko'a mintu ko'e ko'i | ||
| Theorem | simsa-mintu 342 | {simsa} implies {mintu}. (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ ko'a simsa ko'e ko'i ⊢ ko'a mintu ko'e ko'i | ||
| Syntax | sbsteci 343 |
|
| selbri steci | ||
| Definition | df-steci 344 | Definition of {steci} in terms of {ckaji} and {cmima}. |
| ⊢ go ko'a steci ko'e ko'i gi ge ko'e ckaji ko'a gi ko'e cmima ko'i | ||
| Theorem | stecii 345 | Inference form of df-steci 344 (Contributed by la korvo, 17-Aug-2023.) |
| ⊢ ko'a steci ko'e ko'i ⊢ ge
ko'e ckaji ko'a gi ko'e
cmima ko'i | ||
| Theorem | steciri 346 | Reverse inference form of df-steci 344 (Contributed by la korvo, 17-Aug-2023.) |
| ⊢ ge ko'e ckaji ko'a gi ko'e
cmima ko'i ⊢ ko'a steci ko'e ko'i | ||
| Theorem | stecirii 347 | Reverse inference form of df-steci 344 (Contributed by la korvo, 17-Aug-2023.) |
| ⊢ ko'e ckaji ko'a ⊢ ko'e cmima ko'i ⊢ ko'a steci ko'e ko'i | ||
| Syntax | sbmupli 348 |
|
| selbri mupli | ||
| Definition | df-mupli 349 | Tentative definition of {mupli}. It is worth noting that there is currently a lack of community consensus on whether all elements of mupli3 must satisfy mupli2. |
| ⊢ go ko'a mupli ko'e ko'i gi ge ko'a ckaji ko'e gi ko'a cmima ko'i | ||
| Theorem | muplii 350 | Inference form of df-mupli 349 (Contributed by la korvo, 23-Aug-2023.) |
| ⊢ ko'a mupli ko'e ko'i ⊢ ge
ko'a ckaji ko'e gi ko'a
cmima ko'i | ||
| Theorem | muplili 351 | Inference form of df-mupli 349 (Contributed by la korvo, 23-Aug-2023.) |
| ⊢ ko'a mupli ko'e ko'i ⊢ ko'a ckaji ko'e | ||
| Theorem | mupliiri 352 | Inference form of df-mupli 349 (Contributed by la korvo, 23-Aug-2023.) |
| ⊢ ko'a mupli ko'e ko'i ⊢ ko'a cmima ko'i | ||
| Theorem | mupliri 353 | Reverse inference form of df-mupli 349 (Contributed by la korvo, 23-Aug-2023.) |
| ⊢ ge ko'a ckaji ko'e gi ko'a
cmima ko'i ⊢ ko'a mupli ko'e ko'i | ||
| Theorem | muplirii 354 | Reverse inference form of df-mupli 349 (Contributed by la korvo, 23-Aug-2023.) |
| ⊢ ko'a ckaji ko'e ⊢ ko'a cmima ko'i ⊢ ko'a mupli ko'e ko'i | ||
| Syntax | sbsimxu 355 |
|
| selbri simxu | ||
| Definition | df-simxu 356* | An alternate definition of {simxu} which doesn't use {poi ke'a cmima} for element selection. |
| ⊢ go ko'a simxu ko'e gi ro da zo'u ro de zo'u ganai da .e de cmima ko'a gi da ckini de ko'e | ||
| Theorem | simxui 357* | Inference form of df-simxu 356 (Contributed by la korvo, 23-Aug-2023.) |
| ⊢ ko'a simxu ko'e ⊢ ro
da zo'u ro de zo'u ganai da .e de cmima ko'a gi
da ckini de ko'e | ||
| Theorem | simxuri 358* | Reverse inference form of df-simxu 356 (Contributed by la korvo, 23-Aug-2023.) |
| ⊢ ro da zo'u ro de zo'u ganai da .e de cmima ko'a gi
da ckini de ko'e ⊢ ko'a simxu ko'e | ||
| Syntax | sbt 359 | If {bu'a} is a selbri, then so is {te bu'a}. |
| selbri te bu'a | ||
| Definition | df-te 360 | Definition of {te} as a swap of terbri. |
| ⊢ go ko'i te bu'a ko'e ko'a gi ko'a bu'a ko'e ko'i | ||
| Theorem | tei 361 | Inference form of df-te 360 (Contributed by la korvo, 18-Jul-2023.) |
| ⊢ ko'i te bu'a
ko'e ko'a ⊢ ko'a bu'a ko'e ko'i | ||
| Theorem | teri 362 | Reverse inference form of df-te 360 (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 363 | {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 364* | 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 365* | 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 366* | 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 367* | 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 368* | 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 369 |
|
| sumti ko'a ce ko'e | ||
| Definition | df-ce 370 | 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 371 | Inference form of df-ce 370 (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 372 | Reverse inference form of df-ce 370 (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 373 | Inference from composition of ga-lin 142 and ceri 372 (Contributed by la korvo, 5-Aug-2023.) |
| ⊢ ko'a du ko'e ⊢ ko'a cmima ko'e ce ko'i | ||
| Theorem | ceri-rin 374 | Inference from composition of ga-rin 143 and ceri 372 (Contributed by la korvo, 5-Aug-2023.) |
| ⊢ ko'a du ko'i ⊢ ko'a cmima ko'e ce ko'i | ||
| Theorem | ce-left 375 | 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 376 | 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 377 | Syntax for first-order existential quantification. |
| bridi su'o da zo'u broda | ||
| Syntax | bsb 378 | Syntax for second-order existential quantification. |
| bridi su'o bu'a zo'u broda | ||
| Axiom | ax-ex 379* | The axiom of existence: at least one element exists in the universe. This is necessary if we want to exclude the trivial empty model. |
| ⊢ su'o da zo'u da du de | ||
| Theorem | exv 380* | A weaker version of ax-ex 379 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 381 | {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 382 | Inference form of ax-eb 381 (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 383 | 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 384 | Inference form of ax-eq 383 (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 385 | Reduced inference from ax-eq 383 (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 386 | Due to ax-ex 379 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 | ||
| Axiom | ax-cmima-nul 387* | 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 | bsub 388 | 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 389 | 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 390 | Inference form of df-sub 389 (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 391 | 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 392 |
|
| ⊢ ganai da du ko'a gi ganai broda gi [ ko'a / da ] broda | ||
| Theorem | subeq-lem2 393 |
|
| ⊢ ganai da du ko'a gi ganai [ ko'a / da ] broda gi broda | ||
| Theorem | subid 394 | An identity for substitutions. (Contributed by la korvo, 22-Jun-2024.) |
| ⊢ go [ da / da ] broda gi broda | ||
| Syntax | bnd 395 | Syntax for first-order not-free quantification. |
| bridi na'a'u da zo'u broda | ||
| Definition | df-nahahu 396 | 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 397 | bi-rev 80 with generalization on the RHS. (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ go broda gi ro da zo'u brode ⊢ brode ⊢ broda | ||
| Theorem | nfi 398 | Inference form of df-nahahu 396 (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ ganai broda gi ro da zo'u broda ⊢
na'a'u da zo'u broda | ||
| Theorem | nfr 399 | 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 400 | Inference form of nfr 399 (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ na'a'u da zo'u broda ⊢ ganai
broda gi ro da zo'u broda | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |