P. 4 of Theorem List - brismu bridi

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

**Theorem List for brismu bridi -** 301-400 *Has distinct variable group(s)
Type	Label	Description
Statement

Theorem	minturi 301	Reverse inference form of df-mintu 299 (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 302	{mintu} is reflexive over any mintu3. (Contributed by la korvo, 14-Aug-2024.)
⊢ ko'a mintu ko'a ko'e

Theorem	mintu-sym 303	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 304	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 305	{simsa} implies {mintu}. (Contributed by la korvo, 25-Jun-2024.)
⊢ ko'a simsa ko'e ko'i ⊢ ko'a mintu ko'e ko'i

2.3.8 {steci}

Syntax	sbsteci 306
selbri steci

Definition	df-steci 307	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 308	Inference form of df-steci 307 (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 309	Reverse inference form of df-steci 307 (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 310	Reverse inference form of df-steci 307 (Contributed by la korvo, 17-Aug-2023.)
⊢ ko'e ckaji ko'a ⊢ ko'e cmima ko'i ⊢ ko'a steci ko'e ko'i

2.3.9 {mupli}

Syntax	sbmupli 311
selbri mupli

Definition	df-mupli 312	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 313	Inference form of df-mupli 312 (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 314	Inference form of df-mupli 312 (Contributed by la korvo, 23-Aug-2023.)
⊢ ko'a mupli ko'e ko'i ⊢ ko'a ckaji ko'e

Theorem	mupliiri 315	Inference form of df-mupli 312 (Contributed by la korvo, 23-Aug-2023.)
⊢ ko'a mupli ko'e ko'i ⊢ ko'a cmima ko'i

Theorem	mupliri 316	Reverse inference form of df-mupli 312 (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 317	Reverse inference form of df-mupli 312 (Contributed by la korvo, 23-Aug-2023.)
⊢ ko'a ckaji ko'e ⊢ ko'a cmima ko'i ⊢ ko'a mupli ko'e ko'i

2.3.10 {simxu}

Syntax	sbsimxu 318
selbri simxu

Definition	df-simxu 319*	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 320*	Inference form of df-simxu 319 (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 321*	Reverse inference form of df-simxu 319 (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

2.4 Conversion II: {te}

Syntax	sbt 322	If {bu'a} is a selbri, then so is {te bu'a}.
selbri te bu'a

Definition	df-te 323	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 324	Inference form of df-te 323 (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 325	Reverse inference form of df-te 323 (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 326	{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 327*	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 328*	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 329*	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 330*	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 331*	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

2.5 Pairing: {ce}

Syntax	sce 332
sumti ko'a ce ko'e

Definition	df-ce 333	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 334	Inference form of df-ce 333 (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 335	Reverse inference form of df-ce 333 (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 336	Inference from composition of ga-lin 132 and ceri 335 (Contributed by la korvo, 5-Aug-2023.)
⊢ ko'a du ko'e ⊢ ko'a cmima ko'e ce ko'i

Theorem	ceri-rin 337	Inference from composition of ga-rin 133 and ceri 335 (Contributed by la korvo, 5-Aug-2023.)
⊢ ko'a du ko'i ⊢ ko'a cmima ko'e ce ko'i

Theorem	ce-left 338	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 339	Assertion for right-hand component of a {ce} union. (Contributed by la korvo, 5-Aug-2023.)
⊢ ko'e cmima ko'a ce ko'e

2.6 Existential quantifiers I: {su'o}

Syntax	bsd 340	Syntax for first-order existential quantification.
bridi broda bridi su'o da zo'u broda

Syntax	bsb 341	Syntax for second-order existential quantification.
bridi broda bridi su'o bu'a zo'u broda

Axiom	ax-ex 342*	The axiom of existence: at least one element exists in the universe. This is necessary if we want to exclude the trivial empty model. Axiom ax-i9 in [ILE] p. 0.
⊢ su'o da zo'u da du de

Axiom	ax-eb 343	{su'o da zo'u} binds {da}. Axiom ax-ie1 in [ILE] p. 0.
⊢ ganai su'o da zo'u broda gi ro da zo'u su'o da zo'u broda

Theorem	ebi 344	Inference form of ax-eb 343 (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 345	Extensional definition of existential quantification in terms of universal quantification. Axiom ax-ie2 in [ILE] p. 0.
⊢ 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 346	Inference form of ax-eq 345 (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 347	Reduced inference from ax-eq 345 Theorem 19.23h in [ILE] p. 0. (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 348	Due to ax-ex 342 there will always be a spurious witness to any true bridi. Theorem 19.8a in [ILE] p. 0. (Contributed by la korvo, 23-Jun-2024.)
⊢ ganai broda gi su'o da zo'u broda

2.7 Substitution

Syntax	bsub 349	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 350	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 351	Inference form of df-sub 350 (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 352	Property of proper substitution. Theorem sb1 in [ILE] p. 0. (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 353
⊢ ganai da du ko'a gi ganai broda gi [ ko'a / da ] broda

Theorem	subeq-lem2 354
⊢ ganai da du ko'a gi ganai [ ko'a / da ] broda gi broda

Theorem	subid 355	An identity for substitutions. Theorem sbid in [ILE] p. 0. (Contributed by la korvo, 22-Jun-2024.)
⊢ go [ da / da ] broda gi broda

2.8 Not-free quantification

Syntax	bnd 356	Syntax for first-order not-free quantification.
bridi broda bridi na'a'u da zo'u broda

Definition	df-nahahu 357	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 358	bi-rev 70 with generalization on the RHS. Theorem mpgbir in [ILE] p. 0. (Contributed by la korvo, 25-Jun-2024.)
⊢ go broda gi ro da zo'u brode ⊢ brode ⊢ broda

Theorem	nfi 359	Inference form of df-nahahu 357 (Contributed by la korvo, 25-Jun-2024.)
⊢ ganai broda gi ro da zo'u broda ⊢ na'a'u da zo'u broda

Theorem	nfr 360	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 361	Inference form of nfr 360 (Contributed by la korvo, 25-Jun-2024.)
⊢ na'a'u da zo'u broda ⊢ ganai broda gi ro da zo'u broda

Theorem	hbth 362	Hypothesis builder: theorems are closed. (Contributed by la korvo, 25-Jun-2024.)
⊢ broda ⊢ ganai broda gi ro da zo'u broda

Theorem	nfth 363	Theorems are closed. (Contributed by la korvo, 25-Jun-2024.)
⊢ broda ⊢ na'a'u da zo'u broda

Theorem	nfnth 364	Non-theorems are closed. (Contributed by la korvo, 25-Jun-2024.)
⊢ naku zo'u broda ⊢ na'a'u da zo'u broda

Theorem	ceihi-nf 365	The true relation is closed. Theorem nftru in [ILE] p. 0. (Contributed by la korvo, 25-Jun-2024.)
⊢ na'a'u da zo'u cei'i

2.9 Sets II: {zilcmi}

2.9.1 {zilcmi}

Syntax	sbzilcmi 366
selbri zilcmi

Definition	df-zilcmi 367	{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 368	The empty set is a set. (Contributed by la korvo, 19-Sep-2024.)
⊢ le nomei ku zilcmi

Theorem	cmima-zilcmi 369	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 370	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 371	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 372	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 373	Inference form of df-poi-ro 372 (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 374	Reverse inference form of df-poi-ro 372 (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 375	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 376	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 377*
bridi ro bu'a cu bu'e

Definition	df-ro-quant 378*	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 379*	Inference form of df-ro-quant 378 (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 380*	Reverse inference form of df-ro-quant 378 (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

2.10.1 {po'u}

Syntax	brdpu 381	Restriction for first-order identity.
bridi ro da zo'u broda bridi ro da po'u ko'a zo'u broda

Definition	df-pohu 382	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 383
selbri kampu

Definition	df-kampu 384	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 385	Inference form of df-kampu 384 (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 386	Reverse inference form of df-kampu 384 (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 387
sumti ko'a jo'e ko'e

Definition	df-johe 388	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 389	Inference form of df-johe 388 (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 390	Reverse inference form of df-johe 388 (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 391
sumti ko'a ku'a ko'e

Definition	df-kuha 392	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 393	Inference form of df-kuha 392 (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 394	Reverse inference form of df-kuha 392 (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 395	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 396
sumti ko'a ce'o ko'e

Syntax	sbbridi 397
selbri bridi

Definition	df-bridi-u 398
⊢ 1 du'u ko'a bu'a kei bridi 1 ka ce'u bu'a kei ko'a

Definition	df-bridi-b 399
⊢ 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 400
⊢ 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

< 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-774

< Previous Next >