P. 5 of Theorem List - brismu bridi

Home	brismu bridi Theorem List (p. 5 of 10)	< Previous Next >
		Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List

**Theorem List for brismu bridi -** 401-500 *Has distinct variable group(s)
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

2.9 Sets II: {zilcmi}

2.9.1 {zilcmi}

Syntax	sbzilcmi 407
selbri zilcmi

Definition	df-zilcmi 408	{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 zilcmi gi ga ko'a du le nomei ku gi su'o da zo'u da cmima ko'a

Theorem	zilcmi-nomei 409	The empty set is a set. (Contributed by la korvo, 19-Sep-2024.)
⊢ le nomei ku zilcmi

Theorem	cmima-zilcmi 410	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

2.10 Relative clauses I: {poi}, {ke'a}, {ku'o}

Syntax	brdp 411	Restriction for first-order universal quantification.
bridi ro da poi ke'a bo'a ku'o zo'u broda

Syntax	bsdp 412	Restriction for first-order universal quantification.
bridi su'o da poi ke'a bo'a ku'o zo'u broda

Definition	df-poi-ro 413	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 414	Inference form of df-poi-ro 413 (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 415	Reverse inference form of df-poi-ro 413 (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 416	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 417	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 418*
bridi ro bu'a cu bu'e

Definition	df-ro-quant 419*	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 420*	Inference form of df-ro-quant 419 (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 421*	Reverse inference form of df-ro-quant 419 (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

Axiom	ax-cmima-coll 422*	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

2.10.1 {po'u}

Syntax	brdpu 423	Restriction for first-order identity.
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

2.11 Internal hom II: {kampu}

2.11.1 {kampu}

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

2.12 Union: {jo'e}

2.12.1 {jo'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

2.13 Intersection: {ku'a}

2.13.1 {ku'a}

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

2.14 Internal bridi The abstractor {du'u} contains any {ka} abstractions which are closed. Our reasoning for {1 ka} quantification extends to {1 du'u} quantification.

2.14.1 {du'u}

Syntax	sdu 437	If {broda} is a bridi, then {1 du'u} captures it as a sumti.
sumti 1 du'u broda kei

2.14.2 {bridi}

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

Theorem	selbrii 446	Inference form of df-selbri 445 (Contributed by la korvo, 15-Jun-2025.)
⊢ ko'a selbri ko'e ko'i ⊢ ko'a se bridi ko'e ko'i

Theorem	selbriri 447	Reverse inference form of df-selbri 445 (Contributed by la korvo, 15-Jun-2025.)
⊢ ko'a se bridi ko'e ko'i ⊢ ko'a selbri ko'e ko'i

2.14.3 {fatci}

Syntax	sbfatci 448
selbri fatci

Definition	df-fatci 449	Definition of {fatci} in terms of {du'u}.
⊢ go 1 du'u broda kei fatci gi broda

Theorem	fatcii 450	Inference form of df-fatci 449 (Contributed by la korvo, 10-Mar-2024.)
⊢ 1 du'u broda kei fatci ⊢ broda

Theorem	fatciri 451	Reverse inference form of df-fatci 449 (Contributed by la korvo, 10-Mar-2024.)
⊢ broda ⊢ 1 du'u broda kei fatci

Theorem	fatci-ceihi 452	{cei'i} is absolutely true when abstracted. (Contributed by la korvo, 10-Mar-2024.)
⊢ 1 du'u cei'i kei fatci

2.14.4 {nibli}

Syntax	sbnibli 453
selbri nibli

Definition	df-nibli 454	{nibli} internalizes implication.
⊢ go 1 du'u broda kei nibli 1 du'u brode kei gi ganai broda gi brode

Theorem	niblii 455	Inference form of df-nibli 454 (Contributed by la korvo, 19-Jul-2024.)
⊢ 1 du'u broda kei nibli 1 du'u brode kei ⊢ ganai broda gi brode

Theorem	nibliii 456	Inference form of df-nibli 454 (Contributed by la korvo, 19-Jul-2024.)
⊢ 1 du'u broda kei nibli 1 du'u brode kei ⊢ broda ⊢ brode

Theorem	nibliri 457	Reverse inference form of df-nibli 454 (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 458	{nibli} is reflexive. (Contributed by la korvo, 19-Jul-2024.)
⊢ 1 du'u broda kei nibli 1 du'u broda kei

2.14.5 {sigda}

Syntax	sbsigda 459
selbri sigda

Definition	df-sigda 460	{sigda} internalizes implication.
⊢ 1 du'u ganai broda gi brode kei sigda 1 du'u broda kei 1 du'u brode kei

2.14.6 {tsida}

Syntax	sbtsida 461
selbri tsida

Definition	df-tsida 462	{tsida} internalizes biimplication.
⊢ 1 du'u go broda gi brode kei tsida 1 du'u broda kei 1 du'u brode kei

2.14.7 {kanxe}

Syntax	sbkanxe 463
selbri kanxe

Definition	df-kanxe 464	{kanxe} internalizes conjunction.
⊢ 1 du'u ge broda gi brode kei kanxe 1 du'u broda kei 1 du'u brode kei

2.14.8 {vlina}

Syntax	sbvlina 465
selbri vlina

Definition	df-vlina 466	{vlina} internalizes disjunction.
⊢ 1 du'u ga broda gi brode kei vlina 1 du'u broda kei 1 du'u brode kei

2.14.9 {nalti}

Syntax	sbnalti 467
selbri nalti

Definition	df-nalti-ana 468	{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 469	{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

2.15 Parallel reasoning: {fa'u}

2.15.1 {fa'u}

Syntax	sfahu 470
sumti ko'a fa'u ko'e

Definition	df-fahu 471	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 472	Inference form of df-fahu 471 (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 473	Inference form of df-fahu 471 (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 474	Inference form of df-fahu 471 (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 475	Reverse inference form of df-fahu 471 (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

2.16 Deletion: {zi'o}

Syntax	sziho 476
sumti zi'o

Definition	df-ziho 477	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 478	Inference form of df-ziho 477 (Contributed by la korvo, 22-Aug-2024.)
⊢ ko'a bo'a ⊢ zi'o bo'a

Theorem	zihoit 479	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

2.17 Properties of relations We investigate several common non-familial properties of relations.

2.17.1 Transitivity: {takni}

Syntax	sbtakni 480
selbri takni

Definition	df-takni 481*	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 482*	Inference form of df-takni 481 (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

2.17.2 Symmetry: {kinfi}

Syntax	sbkinfi 483
selbri kinfi

Definition	df-kinfi 484*	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 485*	Reverse inference form of df-kinfi 484 (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

2.17.3 Reflexivity: {kinra}

Syntax	sbkinra 486
selbri kinra

Definition	df-kinra 487	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 488	Reverse inference form of df-kinra 487 (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 489	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 490	{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 491	{gripau} is reflexive over any domain. (Contributed by la korvo, 19-Jul-2024.)
⊢ 1 ka ce'u gripau ce'u kei kinra ko'e

2.17.4 Euclidean: {efklipi}, {efklizu}

Syntax	sbefklipi 492
selbri efklipi

Syntax	sbefklizu 493
selbri efklizu

Definition	df-efklipi 494*	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 495*	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 496	Every Euclidean reflexive relation is symmetric.
⊢ ganai ko'a kinra je efklipi ko'e gi ko'a kinfi ko'e

Axiom	ax-efklizu-sym 497
⊢ ganai ko'a kinra je efklizu ko'e gi ko'a kinfi ko'e

2.18 Existential quantifiers II: {pa da}

Syntax	bpd 498	Syntax for uniqueness quantification.
bridi 1 da zo'u broda

Definition	df-pa-da 499	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 500	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

< Previous Next >

Page List Jump to page: Contents 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-977

< Previous Next >