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	gonaiil 301	Inference form of df-gonai 299 (Contributed by la korvo, 8-Aug-2023.)
⊢ gonai broda gi brode ⊢ ga broda gi brode

Theorem	gonaiir 302	Inference form of df-gonai 299 (Contributed by la korvo, 8-Aug-2023.)
⊢ gonai broda gi brode ⊢ naku ge broda gi brode

Theorem	gonairi 303	Reverse inference form of df-gonai 299 (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 304
sumti ko'a .onai ko'e

Definition	df-onai 305	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 306	Inference form of df-onai 305 (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 307	Reverse inference form of df-onai 305 (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 308*
selbri bu'a jonai bu'e

Definition	df-jonai 309*	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 310*	Inference form of df-jonai 309 (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 311*	Reverse inference form of df-jonai 309 (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 312
brirebla bo'a gi'onai bo'e

Definition	df-gihonai 313	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 314	Inference form of df-gihonai 313 (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 315	Inference form of df-gihonai 313 (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 316
bridi ga broda ginai brode

Syntax	bgogin 317
bridi go broda ginai brode

Definition	df-ginai-ga 318
⊢ go ga brode ginai broda gi ganai broda gi brode

Definition	df-ginai-go 319
⊢ 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 320
selbri cmima

Syntax	sbselcmi 321
selbri selcmi

Definition	df-selcmi 322
⊢ go ko'a selcmi ko'e gi ko'a se cmima ko'e

Axiom	ax-cmima-ext 323	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 324
sumti le nomei ku

Definition	df-nomei 325	{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 326	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 327
selbri pamei

Definition	df-pamei 328	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 329	Inference form of df-pamei 328 (Contributed by la korvo, 16-May-2024.)
⊢ ko'a pamei ko'e .e ko'i ⊢ ko'e du ko'i

Theorem	pameiii 330	Inference form of df-pamei 328 (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 331	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 332
selbri gripau

Definition	df-gripau 333	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 334	Inference form of df-gripau 333 (Contributed by la korvo, 15-Jul-2024.)
⊢ ko'a gripau ko'e ⊢ ko'i cmima ko'a na.a ko'e

Theorem	gripauri 335	Reverse inference form of df-gripau 333 (Contributed by la korvo, 15-Jul-2024.)
⊢ ko'i cmima ko'a na.a ko'e ⊢ ko'a gripau ko'e

Theorem	gripauis 336	Inference form of df-gripau 333 (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 337	Inference form of df-gripau 333 (Contributed by la korvo, 15-Jul-2024.)
⊢ ko'a gripau ko'e ⊢ ko'i cmima ko'a ⊢ ko'i cmima ko'e

Theorem	gripauris 338	Reverse inference form of df-gripau 333 (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 339	{gripau} is reflexive. (Contributed by la korvo, 15-Jul-2024.)
⊢ ko'a gripau ko'a

Theorem	gripau-trans 340	{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 341
sumti ce'u

Syntax	spk 342	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 ku

2.3.2 {ckaji}

Syntax	sbckaji 343
selbri ckaji

Theorem	bckaji 344	{ckaji} is often found with this conjugation. (Contributed by la korvo, 14-Aug-2023.)
bridi ko'a ckaji pa ka ce'u bo'a ku

Definition	df-ckaji 345	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 ku gi ko'a bo'a

Theorem	ckajii 346	Inference form of df-ckaji 345 (Contributed by la korvo, 17-Jul-2023.)
⊢ ko'a ckaji pa ka ce'u bo'a ku ⊢ ko'a bo'a

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

2.3.3 {ckini}

Syntax	sbckini 348
selbri ckini

Theorem	bckini 349	{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 ku

Definition	df-ckini 350
⊢ go ko'a ckini ko'e pa ka ce'u bu'a ce'u ku gi ko'a bu'a ko'e

Theorem	ckinii 351	Inference form of df-ckini 350 (Contributed by la korvo, 17-Jul-2023.)
⊢ ko'a ckini ko'e pa ka ce'u bu'a ce'u ku ⊢ ko'a bu'a ko'e

Theorem	ckiniri 352	Reverse inference form of df-ckini 350 (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 ku

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

2.3.4 {sefsi}

Syntax	sbsefsi 354
selbri sefsi

Definition	df-sefsi 355	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 356
selbri simsa

Theorem	bsimsa 357	{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 ku

Definition	df-simsa 358	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 359	Inference form of df-simsa 358 (Contributed by la korvo, 6-Aug-2023.)
⊢ ko'a simsa ko'e ko'i ⊢ ko'a .e ko'e ckaji ko'i

Theorem	simsail 360	Inference form of df-simsa 358 (Contributed by la korvo, 6-Aug-2023.)
⊢ ko'a simsa ko'e ko'i ⊢ ko'a ckaji ko'i

Theorem	simsair 361	Inference form of df-simsa 358 (Contributed by la korvo, 6-Aug-2023.)
⊢ ko'a simsa ko'e ko'i ⊢ ko'e ckaji ko'i

Theorem	simsari 362	Reverse inference form of df-simsa 358 (Contributed by la korvo, 6-Aug-2023.)
⊢ ko'a .e ko'e ckaji ko'i ⊢ ko'a simsa ko'e ko'i

Theorem	simsarii 363	Reverse inference form of df-simsa 358 (Contributed by la korvo, 6-Aug-2023.)
⊢ ko'a ckaji ko'i ⊢ ko'e ckaji ko'i ⊢ ko'a simsa ko'e ko'i

Theorem	simsa-sym 364	{simsa} is symmetric. (Contributed by la korvo, 23-Jun-2026.)
⊢ go ko'a simsa ko'e ko'i gi ko'e simsa ko'a ko'i

2.3.6 {dunli}

Syntax	sbdunli 365
selbri dunli

Theorem	bdunli 366	{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 ku

Definition	df-dunli 367	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 368	Inference form of df-dunli 367 (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 369	Reverse inference form of df-dunli 367 (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 370	{dunli} is reflexive over any dunli3. (Contributed by la korvo, 14-Aug-2024.)
⊢ ko'a dunli ko'a ko'e

Theorem	dunli-sym 371	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

Theorem	du-dunli 372	Suggested by CLL definition of {dunli}: {du} is {dunli} without a standard of comparison, which is a stronger condition. See discussion around example 7.2 from [CLL] p. 18. (Contributed by la korvo, 10-Aug-2026.)
⊢ ko'a du ko'e ⊢ ko'a dunli ko'e ko'i

2.3.7 {mintu}

Syntax	sbmintu 373
selbri mintu

Theorem	bmintu 374	{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 ku

Definition	df-mintu 375	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 376	Inference form of df-mintu 375 (Contributed by la korvo, 6-Aug-2023.)
⊢ ko'a mintu ko'e ko'i ⊢ ko'a .o ko'e ckaji ko'i

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

Theorem	mintu-sym 379	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 380	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 381	{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 382
selbri steci

Definition	df-steci 383	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 384	Inference form of df-steci 383 (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 385	Reverse inference form of df-steci 383 (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 386	Reverse inference form of df-steci 383 (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 387
selbri mupli

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

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

Theorem	mupliri 392	Reverse inference form of df-mupli 388 (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 393	Reverse inference form of df-mupli 388 (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 394
selbri simxu

Definition	df-simxu 395*	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 396*	Inference form of df-simxu 395 (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 397*	Reverse inference form of df-simxu 395 (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 398	If {bu'a} is a selbri, then so is {te bu'a}.
selbri te bu'a

Definition	df-te 399	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 400	Inference form of df-te 399 (Contributed by la korvo, 18-Jul-2023.)
⊢ ko'i te bu'a ko'e ko'a ⊢ 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-1080

< Previous Next >