HomeTheorem List (p. 5 of 9)
Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List
| Home |
brismu
bridi Theorem List (p. 5 of 9) |
< Previous Next >
|
|
Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List | ||
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | hbth 401 | Hypothesis builder: theorems are closed. (Contributed by la korvo, 25-Jun-2024.) |
⊢ broda  ⊢ ganai
broda gi ro da zo'u broda | ||
| Theorem | nfth 402 | Theorems are closed. (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ broda ⊢
na'a'u da zo'u broda | ||
| Theorem | nfnth 403 | Non-theorems are closed. (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ naku broda ⊢
na'a'u da zo'u broda | ||
| Theorem | ceihi-nf 404 | The true relation is closed. (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ na'a'u da zo'u cei'i | ||
| Axiom | ax-dgen1 405* | Special case of first-order generalization where the quantified variable does not occur in the bridi. |
| ⊢ ganai broda gi ro da zo'u broda | ||
| Theorem | nfv 406* | If a variable does not occur in a bridi, then it is neither free nor bound in that bridi. (Contributed by la korvo, 3-Jan-2025.) |
| ⊢ na'a'u da zo'u broda | ||
| Axiom | ax-cmima-coll 407* | The Axiom of Collection: If a bridi is inhabited when parameterized over elements of some set, then the inhabitants also form a set. |
| ⊢ na'a'u da zo'u broda ⊢ ganai
ro de poi
ke'a cmima ko'a ku'o zo'u
su'o di zo'u broda gi su'o da zo'u ro de poi ke'a cmima ko'a ku'o
zo'u su'o di
poi ke'a cmima da ku'o zo'u broda | ||
| Syntax | sbzilcmi 408 |
|
| selbri zilcmi | ||
| Definition | df-zilcmi 409 | {zilcmi} is lujvo for {se cmima zi'o}. The effect is to include {le nomei} as a valid set, forming a predicate of possibly-inhabited sets. |
| ⊢ go ko'a zilcmigi ga ko'a du le nomei ku gi su'o da zo'u da cmima ko'a | ||
| Theorem | zilcmi-nomei 410 | The empty set is a set. (Contributed by la korvo, 19-Sep-2024.) |
| ⊢ le nomei ku zilcmi | ||
| Theorem | cmima-zilcmi 411 | Forget the inhabitant of a set. (Contributed by la korvo, 19-Sep-2024.) |
| ⊢ su'o da zo'u da
cmima ko'a ⊢ ko'a zilcmi | ||
| Syntax | brdp 412 | Restriction for first-order universal quantification. |
| bridi ro da zo'u broda bridi
ro da poi
ke'a bo'a ku'o
zo'u broda | ||
| Syntax | bsdp 413 | Restriction for first-order universal quantification. |
| bridi su'o
da zo'u broda bridi
su'o da poi
ke'a bo'a ku'o
zo'u broda | ||
| Definition | df-poi-ro 414 | Definition of {ro da poi} quantifiers as restricted first-order universal quantifiers. |
| ⊢ go ro da poi ke'a bo'a ku'o zo'u broda gi ro da zo'u ganai da bo'a gi broda | ||
| Theorem | poi-roi 415 | Inference form of df-poi-ro 414 (Contributed by la korvo, 11-Aug-2023.) |
| ⊢ ro da poi ke'a bo'a ku'o zo'u broda ⊢ ro
da zo'u ganai da bo'a gi
broda | ||
| Theorem | poi-rori 416 | Reverse inference form of df-poi-ro 414 (Contributed by la korvo, 11-Aug-2023.) |
| ⊢ ro da zo'u ganai da bo'a gi
broda ⊢
ro da poi
ke'a bo'a ku'o
zo'u broda | ||
| Theorem | poi-gen 417 | First-order generalization for restricted quantification. (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ broda ⊢ ro
da poi ke'a bo'a ku'o zo'u broda | ||
| Theorem | ro-poi 418 | Restricted quantification is a special case of universal quantification. (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ ro da zo'u broda ⊢ ro
da poi ke'a bo'a ku'o zo'u broda | ||
| Syntax | brbc 419* |
|
| bridi ro bu'a cu bu'e | ||
| Definition | df-ro-quant 420* | Definition of {ro broda} quantifier as used in colloquial Lojban utterances like {ro broda cu brode}. |
| ⊢ go ro bu'a cu bu'e gi ro da poi ke'a bu'a ku'o zo'u da bu'e | ||
| Theorem | ro-quanti 421* | Inference form of df-ro-quant 420 (Contributed by la korvo, 12-Sep-2023.) |
| ⊢ ro bu'a cu bu'e ⊢ ro
da poi ke'a bu'a ku'o zo'u da bu'e | ||
| Theorem | ro-quantri 422* | Reverse inference form of df-ro-quant 420 (Contributed by la korvo, 12-Sep-2023.) |
| ⊢ ro da poi ke'a bu'a ku'o zo'u da bu'e ⊢ ro bu'a cu bu'e | ||
| Syntax | brdpu 423 | Restriction for first-order identity. |
| bridi ro da zo'u broda bridi
ro da po'u ko'a zo'u broda | ||
| Definition | df-pohu 424 | Definition of {po'u} in terms of {poi du}, as given by example 3.9-10 from [CLL] p. 8. |
| ⊢ go ro da po'u ko'a zo'u broda gi ro da poi ke'a du ko'a ku'o zo'u broda | ||
| Syntax | sbkampu 425 |
|
| selbri kampu | ||
| Definition | df-kampu 426 | Definition of {kampu} in terms of {ckaji} and {cmima}. |
| ⊢ go ko'a kampu ko'e gi ro da poi ke'a cmima ko'e ku'o zo'u da ckaji ko'a | ||
| Theorem | kampui 427 | Inference form of df-kampu 426 (Contributed by la korvo, 17-Aug-2023.) |
| ⊢ ko'a kampu ko'e ⊢ ro
da poi ke'a cmima ko'e ku'o
zo'u da ckaji ko'a | ||
| Theorem | kampuri 428 | Reverse inference form of df-kampu 426 (Contributed by la korvo, 17-Aug-2023.) |
| ⊢ ro da poi ke'a cmima ko'e ku'o
zo'u da ckaji ko'a ⊢ ko'a kampu ko'e | ||
| Syntax | sjohe 429 |
|
| sumti ko'a jo'e ko'e | ||
| Definition | df-johe 430 | Definition of {jo'e} in terms of {ga}. |
| ⊢ go ko'a cmima ko'e jo'e ko'i gi ko'a cmima ko'e .a ko'i | ||
| Theorem | johei 431 | Inference form of df-johe 430 (Contributed by la korvo, 22-Aug-2023.) |
| ⊢ ko'a cmima ko'e jo'e ko'i ⊢ ko'a cmima ko'e .a ko'i | ||
| Theorem | joheri 432 | Reverse inference form of df-johe 430 (Contributed by la korvo, 22-Aug-2023.) |
| ⊢ ko'a cmima ko'e .a ko'i ⊢ ko'a cmima ko'e jo'e ko'i | ||
| Syntax | skuha 433 |
|
| sumti ko'a ku'a ko'e | ||
| Definition | df-kuha 434 | Definition of {ku'a} in terms of {ge}. |
| ⊢ go ko'a cmima ko'e ku'a ko'i gi ko'a cmima ko'e .e ko'i | ||
| Theorem | kuhai 435 | Inference form of df-kuha 434 (Contributed by la korvo, 22-Aug-2023.) |
| ⊢ ko'a cmima ko'e ku'a ko'i ⊢ ko'a cmima ko'e .e ko'i | ||
| Theorem | kuhari 436 | Reverse inference form of df-kuha 434 (Contributed by la korvo, 22-Aug-2023.) |
| ⊢ ko'a cmima ko'e .e ko'i ⊢ ko'a cmima ko'e ku'a ko'i | ||
The abstractor {du'u} contains any {ka} abstractions which are closed. Our reasoning for {1 ka} quantification extends to {1 du'u} quantification. | ||
| Syntax | sdu 437 | If {broda} is a bridi, then {1 du'u} captures it as a sumti. |
| sumti 1 du'u broda kei | ||
| Syntax | sceho 438 |
|
| sumti ko'a ce'o ko'e | ||
| Syntax | sbbridi 439 |
|
| selbri bridi | ||
| Definition | df-bridi-u 440 |
|
| ⊢ 1 du'u ko'a bu'a kei bridi 1 ka ce'u bu'a kei ko'a | ||
| Definition | df-bridi-b 441 |
|
| ⊢ 1 du'u ko'a bu'a ko'e kei bridi 1 ka ce'u bu'a ce'u kei ko'a ce'o ko'e | ||
| Definition | df-bridi-t 442 |
|
| ⊢ 1 du'u ko'a bu'a ko'e ko'i kei bridi 1 ka ce'u bu'a ce'u ce'u kei ko'a ce'o ko'e ce'o ko'i | ||
| Definition | df-bridi-q 443 |
|
| ⊢ 1 du'u ko'a bu'a ko'e ko'i ko'o kei bridi 1 ka ce'u bu'a ce'u ce'u ce'u kei ko'a ce'o ko'e ce'o ko'i ce'o ko'o | ||
| Syntax | sbselbri 444 |
|
| selbri selbri | ||
| Definition | df-selbri 445 |
|
| ⊢ go ko'a selbri ko'e ko'i gi ko'a se bridi ko'e ko'i | ||
| Syntax | sbfatci 446 |
|
| selbri fatci | ||
| Definition | df-fatci 447 | Definition of {fatci} in terms of {du'u}. |
| ⊢ go 1 du'u broda kei fatci gi broda | ||
| Theorem | fatcii 448 | Inference form of df-fatci 447 (Contributed by la korvo, 10-Mar-2024.) |
| ⊢ 1
du'u broda kei fatci ⊢ broda | ||
| Theorem | fatciri 449 | Reverse inference form of df-fatci 447 (Contributed by la korvo, 10-Mar-2024.) |
| ⊢ broda ⊢ 1 du'u broda
kei fatci | ||
| Theorem | fatci-ceihi 450 | {cei'i} is absolutely true when abstracted. (Contributed by la korvo, 10-Mar-2024.) |
| ⊢ 1 du'u cei'i kei fatci | ||
| Syntax | sbnibli 451 |
|
| selbri nibli | ||
| Definition | df-nibli 452 | {nibli} internalizes implication. |
| ⊢ go 1 du'u broda kei nibli 1 du'u brode kei gi ganai broda gi brode | ||
| Theorem | niblii 453 | Inference form of df-nibli 452 (Contributed by la korvo, 19-Jul-2024.) |
| ⊢ 1
du'u broda kei nibli 1 du'u brode kei ⊢ ganai broda gi brode | ||
| Theorem | nibliii 454 | Inference form of df-nibli 452 (Contributed by la korvo, 19-Jul-2024.) |
⊢ 1
du'u broda kei nibli 1 du'u brode kei  ⊢ broda ⊢ brode | ||
| Theorem | nibliri 455 | Reverse inference form of df-nibli 452 (Contributed by la korvo, 19-Jul-2024.) |
| ⊢ ganai broda gi brode ⊢ 1 du'u broda
kei nibli 1
du'u brode
kei | ||
| Theorem | nibli-refl 456 | {nibli} is reflexive. (Contributed by la korvo, 19-Jul-2024.) |
| ⊢ 1 du'u broda kei nibli 1 du'u broda kei | ||
| Syntax | sbsigda 457 |
|
| selbri sigda | ||
| Definition | df-sigda 458 | {sigda} internalizes implication. |
| ⊢ 1 du'u ganai broda gi brode kei sigda 1 du'u broda kei 1 du'u brode kei | ||
| Syntax | sbtsida 459 |
|
| selbri tsida | ||
| Definition | df-tsida 460 | {tsida} internalizes biimplication. |
| ⊢ 1 du'u go broda gi brode kei tsida 1 du'u broda kei 1 du'u brode kei | ||
| Syntax | sbkanxe 461 |
|
| selbri kanxe | ||
| Definition | df-kanxe 462 | {kanxe} internalizes conjunction. |
| ⊢ 1 du'u ge broda gi brode kei kanxe 1 du'u broda kei 1 du'u brode kei | ||
| Syntax | sbvlina 463 |
|
| selbri vlina | ||
| Definition | df-vlina 464 | {vlina} internalizes disjunction. |
| ⊢ 1 du'u ga broda gi brode kei vlina 1 du'u broda kei 1 du'u brode kei | ||
| Syntax | sbnalti 465 |
|
| selbri nalti | ||
| Definition | df-nalti-ana 466 | {nalti} internalizes negation. This direction adds the {naku} prenex to the second bridi. |
| ⊢ 1 du'u broda kei nalti 1 du'u naku broda kei | ||
| Definition | df-nalti-kata 467 | {nalti} internalizes negation. This direction adds the {naku} prenex to the first bridi. |
| ⊢ 1 du'u naku broda kei nalti 1 du'u broda kei | ||
| Syntax | sfahu 468 |
|
| sumti ko'a fa'u ko'e | ||
| Definition | df-fahu 469 | Definition of {fa'u} in terms of {ge}. |
| ⊢ go ko'a fa'u ko'e bu'a ko'i fa'u ko'o gi ge ko'a bu'a ko'i gi ko'e bu'a ko'o | ||
| Theorem | fahui 470 | Inference form of df-fahu 469 (Contributed by la korvo, 16-Jun-2024.) |
| ⊢ ko'a fa'u ko'e
bu'a ko'i
fa'u ko'o ⊢ ge ko'a bu'a ko'i gi ko'e
bu'a ko'o | ||
| Theorem | fahuil 471 | Inference form of df-fahu 469 (Contributed by la korvo, 16-Jun-2024.) |
| ⊢ ko'a fa'u ko'e
bu'a ko'i
fa'u ko'o ⊢ ko'a bu'a ko'i | ||
| Theorem | fahuir 472 | Inference form of df-fahu 469 (Contributed by la korvo, 16-Jun-2024.) |
| ⊢ ko'a fa'u ko'e
bu'a ko'i
fa'u ko'o ⊢ ko'e bu'a ko'o | ||
| Theorem | fahuri 473 | Reverse inference form of df-fahu 469 (Contributed by la korvo, 16-Jun-2024.) |
| ⊢ ko'a bu'a ko'i ⊢ ko'e bu'a ko'o ⊢ ko'a fa'u ko'e
bu'a ko'i
fa'u ko'o | ||
| Syntax | sziho 474 |
|
| sumti zi'o | ||
| Definition | df-ziho 475 | Definition of {zi'o}. Justified by example 7.4-7 from [CLL] p. 7. |
| ⊢ ganai ko'a bo'a gi zi'o bo'a | ||
| Theorem | zihoi 476 | Inference form of df-ziho 475 (Contributed by la korvo, 22-Aug-2024.) |
| ⊢ ko'a bo'a ⊢ zi'o bo'a | ||
| Theorem | zihoit 477 | Delete the second place of a binary bridi. (Contributed by la korvo, 22-Aug-2024.) |
| ⊢ ko'a bu'a ko'e ⊢ ko'a bu'a zi'o | ||
We investigate several common non-familial properties of relations. | ||
| Syntax | sbtakni 478 |
|
| selbri takni | ||
| Definition | df-takni 479* | A standard definition of transitive relations. |
| ⊢ go ko'a takni ko'e gi ro da poi ke'a cmima ko'e ku'o zo'u ro de poi ke'a cmima ko'e ku'o zo'u ro di poi ke'a cmima ko'e ku'o zo'u ganai ge da ckini de ko'a gi de ckini di ko'a gi da ckini di ko'a | ||
| Theorem | taknii 480* | Inference form of df-takni 479 (Contributed by la korvo, 22-Jun-2024.) |
| ⊢ ko'a takni ko'e ⊢ ro
da poi ke'a cmima ko'e ku'o
zo'u ro de
poi ke'a cmima ko'e ku'o zo'u
ro di poi
ke'a cmima ko'e ku'o zo'u
ganai ge da ckini de ko'a gi de
ckini di ko'a gi da
ckini di ko'a | ||
| Syntax | sbkinfi 481 |
|
| selbri kinfi | ||
| Definition | df-kinfi 482* | A standard definition of symmetric relations. |
| ⊢ go ko'a kinfi ko'e gi ro da poi ke'a cmima ko'e ku'o zo'u ro de poi ke'a cmima ko'e ku'o zo'u ganai da ckini de ko'a gi de ckini da ko'a | ||
| Theorem | kinfiri 483* | Reverse inference form of df-kinfi 482 (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ ro da poi ke'a cmima ko'e ku'o
zo'u ro de
poi ke'a cmima ko'e ku'o zo'u
ganai da ckini de ko'a gi de
ckini da ko'a ⊢ ko'a kinfi ko'e | ||
| Syntax | sbkinra 484 |
|
| selbri kinra | ||
| Definition | df-kinra 485 | A standard definition of reflexive relations. |
| ⊢ go ko'a kinra ko'e gi ro da poi ke'a cmima ko'e ku'o zo'u da ckini da ko'a | ||
| Theorem | kinrari 486 | Reverse inference form of df-kinra 485 (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ ro da poi ke'a cmima ko'e ku'o
zo'u da ckini da ko'a ⊢ ko'a kinra ko'e | ||
| Theorem | refl-kinra 487 | If a selbri is reflexive over any metasyntactic terbri, then it is reflexive over any domain. (Contributed by la korvo, 13-Aug-2024.) |
| ⊢ da
bu'a da ⊢ 1 ka ce'u bu'a ce'u kei kinra ko'e | ||
| Theorem | du-kinra 488 | {du} is reflexive over any domain. (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ 1 ka ce'u du ce'u kei kinra ko'e | ||
| Theorem | gripau-kinra 489 | {gripau} is reflexive over any domain. (Contributed by la korvo, 19-Jul-2024.) |
| ⊢ 1 ka ce'u gripau ce'u kei kinra ko'e | ||
| Syntax | sbefklipi 490 |
|
| selbri efklipi | ||
| Syntax | sbefklizu 491 |
|
| selbri efklizu | ||
| Definition | df-efklipi 492* | A standard definition of right-Euclidean relations. |
| ⊢ go ko'a efklipi ko'e gi ro da poi ke'a cmima ko'e ku'o zo'u ro de poi ke'a cmima ko'e ku'o zo'u ro di poi ke'a cmima ko'e ku'o zo'u ganai da ckini de .e di ko'a gi de ckini di ko'a | ||
| Definition | df-efklizu 493* | A standard definition of left-Euclidean relations. |
| ⊢ go ko'a efklizu ko'e gi ro da poi ke'a cmima ko'e ku'o zo'u ro de poi ke'a cmima ko'e ku'o zo'u ro di poi ke'a cmima ko'e ku'o zo'u ganai de .e di ckini da ko'a gi de ckini di ko'a | ||
| Axiom | ax-efklipi-sym 494 | Every Euclidean reflexive relation is symmetric. |
| ⊢ ganai ko'a kinra je efklipi ko'e gi ko'a kinfi ko'e | ||
| Axiom | ax-efklizu-sym 495 |
|
| ⊢ ganai ko'a kinra je efklizu ko'e gi ko'a kinfi ko'e | ||
| Syntax | bpd 496 | Syntax for uniqueness quantification. |
| bridi 1 da zo'u broda | ||
| Definition | df-pa-da 497 | Definition of {1 da} in terms of {su'o da} and {du}. |
| ⊢ go 1 da zo'u da bo'a gi su'o da zo'u ge da bo'a gi ganai ko'a bo'a gi ko'a du da | ||
| Theorem | pa-dai 498 | Inference form of pa-da (future) (Contributed by la korvo, 20-Aug-2023.) |
| ⊢ 1
da zo'u da bo'a ⊢ su'o
da zo'u ge da bo'a gi
ganai ko'a bo'a gi ko'a
du da | ||
| Theorem | pa-dari 499 | Reverse inference form of pa-da (future) (Contributed by la korvo, 20-Aug-2023.) |
| ⊢ su'o da zo'u ge da bo'a gi
ganai ko'a bo'a gi ko'a
du da ⊢ 1 da zo'u da bo'a | ||
| Syntax | bpdp 500 | Restriction for first-order uniqueness quantification. |
| bridi 1 da zo'u broda bridi 1 da poi
ke'a bo'a ku'o
zo'u broda | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |