![]() |
brismu
bridi Theorem List (p. 4 of 11) |
< Previous Next >
|
Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | gonaiir 301 | Inference form of df-gonai 298 (Contributed by la korvo, 8-Aug-2023.) |
⊢ gonai broda gi brode ![]() | ||
Theorem | gonairi 302 | Reverse inference form of df-gonai 298 (Contributed by la korvo, 8-Aug-2023.) |
⊢ ge
ga broda gi brode gi naku
ge broda gi brode ![]() | ||
Syntax | sjonai 303 |
|
sumti ko'a .onai ko'e | ||
Definition | df-onai 304 | Definition of {.onai} in terms of {gonai}. By analogy with forethought version of example 12.2-5 from [CLL] p. 14. |
⊢ go ko'a .onai ko'e bo'a gi gonai ko'a bo'a gi ko'e bo'a | ||
Theorem | onaii 305 | Inference form of df-onai 304 (Contributed by la korvo, 16-Aug-2023.) |
⊢ ko'a .onai ko'e
bo'a ![]() | ||
Theorem | onairi 306 | Reverse inference form of df-onai 304 (Contributed by la korvo, 16-Aug-2023.) |
⊢ gonai ko'a bo'a gi
ko'e bo'a ![]() | ||
Syntax | sbjonai 307* |
|
selbri bu'a jonai bu'e | ||
Definition | df-jonai 308* | Definition of {jonai} in terms of {gonai}. By analogy with example 12.2-5 of [CLL] p. 14. |
⊢ go ko'a bu'a jonai bu'e ko'e gi gonai ko'a bu'a ko'e gi ko'a bu'e ko'e | ||
Theorem | jonaii 309* | Inference form of df-jonai 308 (Contributed by la korvo, 16-Aug-2023.) |
⊢ ko'a bu'a
jonai bu'e ko'e ![]() | ||
Theorem | jonairi 310* | Reverse inference form of df-jonai 308 (Contributed by la korvo, 16-Aug-2023.) |
⊢ gonai ko'a bu'a ko'e gi ko'a
bu'e ko'e ![]() | ||
Syntax | tgihonai 311 |
|
brirebla bo'a gi'onai bo'e | ||
Definition | df-gihonai 312 | Definition of {gi'onai} in terms of {gonai}. |
⊢ go ko'a bo'a gi'onai bo'e gi gonai ko'a bo'a gi ko'a bo'e | ||
Theorem | gihonaii 313 | Inference form of df-gihonai 312 (Contributed by la korvo, 14-Aug-2023.) |
⊢ ko'a bo'a
gi'onai bo'e ![]() | ||
Theorem | gihonairi 314 | Inference form of df-gihonai 312 (Contributed by la korvo, 14-Aug-2023.) |
⊢ gonai ko'a bo'a gi
ko'a bo'e ![]() | ||
Syntax | bgagin 315 |
|
bridi ga broda ginai brode | ||
Syntax | bgogin 316 |
|
bridi go broda ginai brode | ||
Definition | df-ginai-ga 317 |
|
⊢ go ga brode ginai broda gi ganai broda gi brode | ||
Definition | df-ginai-go 318 |
|
⊢ go go broda ginai brode gi gonai broda gi brode | ||
We build the various non-logical connectives, which express combinations of elements of relations beyond truth tables. In particular, we develop the notion of set membership. | ||
Syntax | sbcmima 319 |
|
selbri cmima | ||
Syntax | sbselcmi 320 |
|
selbri selcmi | ||
Definition | df-selcmi 321 |
|
⊢ go ko'a selcmi ko'e gi ko'a se cmima ko'e | ||
Axiom | ax-cmima-ext 322 | The Axiom of Extensionality: If no elements differ in elementhood for two sets, then they are the same set. |
⊢ ganai ro da zo'u da cmima ko'a .o ko'e gi ko'a du ko'e | ||
Syntax | snomei 323 |
|
sumti le nomei ku | ||
Definition | df-nomei 324 | {le nomei} is the empty set. Literally it is the set with zero cardinality. By standard folklore of sets, it is unique up to isomorphism, justifying {le}. |
⊢ naku ko'a cmima le nomei ku | ||
Theorem | nomei-gaiho 325 | If the empty set is inhabited, then there is a contradiction. (Contributed by la korvo, 16-May-2024.) |
⊢ ko'a cmima le nomei
ku ![]() | ||
Syntax | sbpamei 326 |
|
selbri pamei | ||
Definition | df-pamei 327 | The singleton set is the unique set whose elements are all isomorphic. Since we use the full semantics of second-order logic, we cannot construct the witness isomorphisms. As a compromise, we construct the isomorphism between any two elements of any particular singleton set. |
⊢ go ko'a pamei ko'e .e ko'i gi ko'e du ko'i | ||
Theorem | pameii 328 | Inference form of df-pamei 327 (Contributed by la korvo, 16-May-2024.) |
⊢ ko'a pamei ko'e .e ko'i ![]() | ||
Theorem | pameiii 329 | Inference form of df-pamei 327 (Contributed by la korvo, 16-May-2024.) |
⊢ ko'a pamei ko'e ![]() ![]() | ||
Axiom | ax-pamei-cmima 330 | The singleton set has one element. |
⊢ ganai ko'a pamei ko'e gi ko'e cmima ko'a | ||
Syntax | sbgripau 331 |
|
selbri gripau | ||
Definition | df-gripau 332 | Definition of {gripau} in terms of {cmima} and {na.a}. Defined in section 7 of [CLL] p. 18 based on the gloss "set-part". This definition is phrased with an implicit universal quantification instead of {ro da zo'u da cmima ko'a na.a ko'e} or {ro da poi ke'a cmima ko'a ku'o zo'u da cmima ko'e} for succinctness and ease of theorem-proving. |
⊢ go ko'a gripau ko'e gi ko'i cmima ko'a na.a ko'e | ||
Theorem | gripaui 333 | Inference form of df-gripau 332 (Contributed by la korvo, 15-Jul-2024.) |
⊢ ko'a gripau ko'e ![]() | ||
Theorem | gripauri 334 | Reverse inference form of df-gripau 332 (Contributed by la korvo, 15-Jul-2024.) |
⊢ ko'i cmima ko'a na.a ko'e ![]() | ||
Theorem | gripauis 335 | Inference form of df-gripau 332 (Contributed by la korvo, 19-Jul-2024.) |
⊢ ko'a gripau ko'e ![]() | ||
Theorem | gripauiis 336 | Inference form of df-gripau 332 (Contributed by la korvo, 15-Jul-2024.) |
⊢ ko'a gripau ko'e ![]() ![]() | ||
Theorem | gripauris 337 | Reverse inference form of df-gripau 332 (Contributed by la korvo, 19-Jul-2024.) |
⊢ ganai ko'i cmima ko'a gi ko'i
cmima ko'e ![]() | ||
Theorem | gripau-refl 338 | {gripau} is reflexive. (Contributed by la korvo, 15-Jul-2024.) |
⊢ ko'a gripau ko'a | ||
Theorem | gripau-trans 339 | {gripau} is transitive. (Contributed by la korvo, 19-Jul-2024.) |
⊢ ko'a gripau ko'e ![]() ![]() | ||
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 {pa ka} quantification in acknowledgement of isomorphism-invariance. | ||
Syntax | sc 340 |
|
sumti ce'u | ||
Syntax | spk 341 | If {bo'a} is a brirebla, then filling its first place with a sumti and wrapping it with {pa ka} yields sumti. |
sumti pa ka ko'a bo'a kei | ||
Syntax | sbckaji 342 |
|
selbri ckaji | ||
Theorem | bckaji 343 | {ckaji} is often found with this conjugation. (Contributed by la korvo, 14-Aug-2023.) |
bridi ko'a ckaji pa ka ce'u bo'a kei | ||
Definition | df-ckaji 344 | Definition of {ckaji} from {ka}. Based on example 4.1-2 of [CLL] p. 11. |
⊢ go ko'a ckaji pa ka ce'u bo'a kei gi ko'a bo'a | ||
Theorem | ckajii 345 | Inference form of df-ckaji 344 (Contributed by la korvo, 17-Jul-2023.) |
⊢ ko'a ckaji pa ka ce'u bo'a kei ![]() | ||
Theorem | ckajiri 346 | Reverse inference form of df-ckaji 344 (Contributed by la korvo, 17-Jul-2023.) |
⊢ ko'a bo'a ![]() | ||
Syntax | sbckini 347 |
|
selbri ckini | ||
Theorem | bckini 348 | {ckini} is often found with this conjugation. (Contributed by la korvo, 14-Aug-2023.) |
bridi ko'a ckini ko'e pa ka ce'u bu'a ce'u kei | ||
Definition | df-ckini 349 |
|
⊢ go ko'a ckini ko'e pa ka ce'u bu'a ce'u kei gi ko'a bu'a ko'e | ||
Theorem | ckinii 350 | Inference form of df-ckini 349 (Contributed by la korvo, 17-Jul-2023.) |
⊢ ko'a ckini ko'e pa ka
ce'u bu'a ce'u
kei ![]() | ||
Theorem | ckiniri 351 | Reverse inference form of df-ckini 349 (Contributed by la korvo, 17-Jul-2023.) |
⊢ ko'a bu'a ko'e ![]() | ||
Theorem | ckini-se 352 | {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 pa ka
ce'u bu'a ce'u
kei ![]() | ||
Syntax | sbsefsi 353 |
|
selbri sefsi | ||
Definition | df-sefsi 354 | 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 355 |
|
selbri simsa | ||
Theorem | bsimsa 356 | {simsa} is often found with this conjugation. (Contributed by la korvo, 6-Aug-2023.) |
bridi ko'a simsa ko'e pa ka ce'u bu'a kei | ||
Definition | df-simsa 357 | 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 358 | Inference form of df-simsa 357 (Contributed by la korvo, 6-Aug-2023.) |
⊢ ko'a simsa ko'e ko'i ![]() | ||
Theorem | simsail 359 | Inference form of df-simsa 357 (Contributed by la korvo, 6-Aug-2023.) |
⊢ ko'a simsa ko'e ko'i ![]() | ||
Theorem | simsair 360 | Inference form of df-simsa 357 (Contributed by la korvo, 6-Aug-2023.) |
⊢ ko'a simsa ko'e ko'i ![]() | ||
Theorem | simsari 361 | Reverse inference form of df-simsa 357 (Contributed by la korvo, 6-Aug-2023.) |
⊢ ko'a .e ko'e
ckaji ko'i ![]() | ||
Theorem | simsarii 362 | Reverse inference form of df-simsa 357 (Contributed by la korvo, 6-Aug-2023.) |
⊢ ko'a ckaji ko'i ![]() ![]() | ||
Axiom | ax-simsa-sym 363 | {simsa} is symmetric. |
⊢ go ko'a simsa ko'e ko'i gi ko'e simsa ko'a ko'i | ||
Syntax | sbdunli 364 |
|
selbri dunli | ||
Theorem | bdunli 365 | {dunli} is often found with this conjugation. (Contributed by la korvo, 23-Jun-2024.) |
bridi ko'a dunli ko'e pa ka ce'u bu'a ce'u kei | ||
Definition | df-dunli 366 | 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 367 | Inference form of df-dunli 366 (Contributed by la korvo, 23-Jun-2024.) |
⊢ ko'a dunli ko'e ko'i ![]() | ||
Theorem | dunliri 368 | Reverse inference form of df-dunli 366 (Contributed by la korvo, 23-Jun-2024.) |
⊢ ko'a .o ko'e
ckini ko'o ko'i ![]() | ||
Theorem | dunli-refl 369 | {dunli} is reflexive over any dunli3. (Contributed by la korvo, 14-Aug-2024.) |
⊢ ko'a dunli ko'a ko'e | ||
Theorem | dunli-sym 370 | 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 371 |
|
selbri mintu | ||
Theorem | bmintu 372 | {mintu} is often found with this conjugation. (Contributed by la korvo, 6-Aug-2023.) |
bridi ko'a mintu ko'e pa ka ce'u bu'a kei | ||
Definition | df-mintu 373 | 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 374 | Inference form of df-mintu 373 (Contributed by la korvo, 6-Aug-2023.) |
⊢ ko'a mintu ko'e ko'i ![]() | ||
Theorem | minturi 375 | Reverse inference form of df-mintu 373 (Contributed by la korvo, 6-Aug-2023.) |
⊢ ko'a .o ko'e
ckaji ko'i ![]() | ||
Theorem | mintu-refl 376 | {mintu} is reflexive over any mintu3. (Contributed by la korvo, 14-Aug-2024.) |
⊢ ko'a mintu ko'a ko'e | ||
Theorem | mintu-sym 377 | 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 378 | 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 ![]() | ||
Theorem | simsa-mintu 379 | {simsa} implies {mintu}. (Contributed by la korvo, 25-Jun-2024.) |
⊢ ko'a simsa ko'e ko'i ![]() | ||
Syntax | sbsteci 380 |
|
selbri steci | ||
Definition | df-steci 381 | 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 382 | Inference form of df-steci 381 (Contributed by la korvo, 17-Aug-2023.) |
⊢ ko'a steci ko'e ko'i ![]() | ||
Theorem | steciri 383 | Reverse inference form of df-steci 381 (Contributed by la korvo, 17-Aug-2023.) |
⊢ ge ko'e ckaji ko'a gi ko'e
cmima ko'i ![]() | ||
Theorem | stecirii 384 | Reverse inference form of df-steci 381 (Contributed by la korvo, 17-Aug-2023.) |
⊢ ko'e ckaji ko'a ![]() ![]() | ||
Syntax | sbmupli 385 |
|
selbri mupli | ||
Definition | df-mupli 386 | 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 387 | Inference form of df-mupli 386 (Contributed by la korvo, 23-Aug-2023.) |
⊢ ko'a mupli ko'e ko'i ![]() | ||
Theorem | muplili 388 | Inference form of df-mupli 386 (Contributed by la korvo, 23-Aug-2023.) |
⊢ ko'a mupli ko'e ko'i ![]() | ||
Theorem | mupliiri 389 | Inference form of df-mupli 386 (Contributed by la korvo, 23-Aug-2023.) |
⊢ ko'a mupli ko'e ko'i ![]() | ||
Theorem | mupliri 390 | Reverse inference form of df-mupli 386 (Contributed by la korvo, 23-Aug-2023.) |
⊢ ge ko'a ckaji ko'e gi ko'a
cmima ko'i ![]() | ||
Theorem | muplirii 391 | Reverse inference form of df-mupli 386 (Contributed by la korvo, 23-Aug-2023.) |
⊢ ko'a ckaji ko'e ![]() ![]() | ||
Syntax | sbsimxu 392 |
|
selbri simxu | ||
Definition | df-simxu 393* | 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 394* | Inference form of df-simxu 393 (Contributed by la korvo, 23-Aug-2023.) |
⊢ ko'a simxu ko'e ![]() | ||
Theorem | simxuri 395* | Reverse inference form of df-simxu 393 (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 ![]() | ||
Syntax | sbt 396 | If {bu'a} is a selbri, then so is {te bu'a}. |
selbri te bu'a | ||
Definition | df-te 397 | 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 398 | Inference form of df-te 397 (Contributed by la korvo, 18-Jul-2023.) |
⊢ ko'i te bu'a
ko'e ko'a ![]() | ||
Theorem | teri 399 | Reverse inference form of df-te 397 (Contributed by la korvo, 18-Jul-2023.) |
⊢ ko'a bu'a ko'e ko'i ![]() | ||
Theorem | te-invo 400 | {te} is an involution. (Contributed by la korvo, 18-Jul-2023.) |
⊢ ko'a te te bu'a ko'e ko'i ![]() |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |