P. 4 of Theorem List - brismu bridi

Home	brismu bridi Theorem List (p. 4 of 9)	< 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	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

2.3 Internal hom 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.

2.3.1 {ka}

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

2.3.2 {ckaji}

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

2.3.3 {ckini}

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

2.3.4 {sefsi}

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

2.3.5 {simsa}

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

2.3.6 {dunli}

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

2.3.7 {mintu}

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

2.3.8 {steci}

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

2.3.9 {mupli}

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

2.3.10 {simxu}

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

2.4 Conversion II: {te}

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

2.5 Pairing: {ce}

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

2.6 Existential quantifiers I: {su'o}

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

Syntax	bsb 378	Syntax for second-order existential quantification.
bridi broda 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

2.7 Substitution

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

2.8 Not-free quantification

Syntax	bnd 395	Syntax for first-order not-free quantification.
bridi broda 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 >

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

< Previous Next >