P. 4 of Theorem List - brismu bridi

Home	brismu bridi Theorem List (p. 4 of 11)	< 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	gonaiir 301	Inference form of df-gonai 298 (Contributed by la korvo, 8-Aug-2023.)
⊢ gonai broda gi brode ⊢ naku ge 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 ⊢ gonai broda gi brode

1.14.2 {.onai}

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 ⊢ gonai ko'a bo'a gi 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 ⊢ ko'a .onai ko'e bo'a

1.14.3 {jonai}

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 ⊢ gonai ko'a bu'a ko'e gi ko'a 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 ⊢ ko'a bu'a jonai bu'e ko'e

1.14.4 {gi'onai}

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 ⊢ gonai ko'a bo'a gi ko'a 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 ⊢ ko'a bo'a gi'onai bo'e

1.15 Extra connectives

1.15.1 {ginai}

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

PART 2 NON-LOGICAL CONNECTIVES 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.

2.1 Sets I: {nomei}, {pamei}

2.1.1 {cmima}

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

2.1.2 {nomei}

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 ⊢ gai'o

2.1.3 {pamei}

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 ⊢ ko'e du ko'i

Theorem	pameiii 329	Inference form of df-pamei 327 (Contributed by la korvo, 16-May-2024.)
⊢ ko'a pamei ko'e ⊢ ko'a pamei ko'i ⊢ ko'e du ko'i

Axiom	ax-pamei-cmima 330	The singleton set has one element.
⊢ ganai ko'a pamei ko'e gi ko'e cmima ko'a

2.2 Subsets

2.2.1 {gripau}

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 ⊢ ko'i cmima ko'a na.a 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 ⊢ ko'a gripau ko'e

Theorem	gripauis 335	Inference form of df-gripau 332 (Contributed by la korvo, 19-Jul-2024.)
⊢ ko'a gripau ko'e ⊢ ganai ko'i cmima ko'a gi ko'i cmima ko'e

Theorem	gripauiis 336	Inference form of df-gripau 332 (Contributed by la korvo, 15-Jul-2024.)
⊢ ko'a gripau ko'e ⊢ ko'i cmima ko'a ⊢ ko'i cmima 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 ⊢ ko'a gripau 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 ⊢ 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 {pa ka} quantification in acknowledgement of isomorphism-invariance.

2.3.1 {ka}

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

2.3.2 {ckaji}

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 ⊢ ko'a bo'a

Theorem	ckajiri 346	Reverse inference form of df-ckaji 344 (Contributed by la korvo, 17-Jul-2023.)
⊢ ko'a bo'a ⊢ ko'a ckaji pa ka ce'u bo'a kei

2.3.3 {ckini}

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 ⊢ ko'a bu'a ko'e

Theorem	ckiniri 351	Reverse inference form of df-ckini 349 (Contributed by la korvo, 17-Jul-2023.)
⊢ ko'a bu'a ko'e ⊢ ko'a ckini ko'e pa ka ce'u bu'a ce'u kei

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 ⊢ ko'e ckini ko'a pa ka ce'u se bu'a ce'u kei

2.3.4 {sefsi}

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

2.3.5 {simsa}

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 ⊢ ko'a .e ko'e ckaji 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 ⊢ ko'a ckaji 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 ⊢ ko'e ckaji 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 ⊢ ko'a simsa ko'e ko'i

Theorem	simsarii 362	Reverse inference form of df-simsa 357 (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 363	{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 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 ⊢ ko'a .o ko'e ckini ko'o 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 ⊢ ko'a dunli ko'e 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

2.3.7 {mintu}

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 ⊢ ko'a .o ko'e ckaji 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 ⊢ ko'a mintu ko'e 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 ⊢ ko'a mintu ko'e ko'i

Theorem	simsa-mintu 379	{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 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 ⊢ ge ko'e ckaji ko'a gi ko'e cmima 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 ⊢ ko'a steci ko'e ko'i

Theorem	stecirii 384	Reverse inference form of df-steci 381 (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 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 ⊢ ge ko'a ckaji ko'e gi ko'a cmima 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 ⊢ ko'a ckaji ko'e

Theorem	mupliiri 389	Inference form of df-mupli 386 (Contributed by la korvo, 23-Aug-2023.)
⊢ ko'a mupli ko'e ko'i ⊢ ko'a cmima 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 ⊢ ko'a mupli ko'e ko'i

Theorem	muplirii 391	Reverse inference form of df-mupli 386 (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 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 ⊢ ro da zo'u ro de zo'u ganai da .e de cmima ko'a gi da ckini de 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 ⊢ ko'a simxu ko'e

2.4 Conversion II: {te}

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 ⊢ ko'a bu'a ko'e ko'i

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 ⊢ ko'i te bu'a ko'e ko'a

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 ⊢ ko'a bu'a ko'e 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-800 9 801-900 10 901-1000 11 1001-1048

< Previous Next >