P. 3 of Theorem List - brismu bridi

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

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

Theorem	duris 201	Sugared reverse inference form of df-du 197 (Contributed by la korvo, 23-Jun-2024.)
⊢ go ko'a bu'a gi ko'e bu'a ⊢ ko'a du ko'e

Theorem	du-refl 202	{du} is reflexive. (Contributed by la korvo, 16-Aug-2023.) (Shortened by la korvo, 23-Jun-2024.)
⊢ ko'a du ko'a

Theorem	du-trans 203	{du} is transitive. (Contributed by la korvo, 16-Aug-2023.) (Shortened by la korvo, 23-Jun-2024.)
⊢ ko'a du ko'e ⊢ ko'e du ko'i ⊢ ko'a du ko'i

Theorem	du-sym 204	{du} is symmetric. (Contributed by la korvo, 16-Aug-2023.) (Shortened by la korvo, 23-Jun-2024.)
⊢ ko'a du ko'e ⊢ ko'e du ko'a

Theorem	se-du-elim 205	{se du} may be replaced with {du}. Theorem Cat.Allegory.Base.dual-id in [1Lab] p. 0. (Contributed by la korvo, 9-Jul-2023.)
⊢ ko'a se du ko'e ⊢ ko'a du ko'e

1.12 Boolean predicates: {cei'i}

Syntax	bceihi 206
bridi cei'i

Definition	df-ceihi 207	The predicate which is always true. Note that both sides are relational: the left-hand side definitionally only has one inhabitant, so this definition asserts that {ko'a du ko'a} is only true via one path.
⊢ go cei'i gi ko'a du ko'a

Theorem	ceihi 208	{cei'i} is always true. (Contributed by la korvo, 18-Jul-2023.)
⊢ cei'i

1.13 Negation I: {gai'o}, {naku} Lojban classically contains a {na} which may slide around in a prenex and between connectives. To be constructive, we will more carefully introduce {naku} negation within the prenex first, and then justify various simplifications and rearrangements.

Syntax	bgaiho 209
bridi gai'o

Syntax	bnk 210	Syntax for negation over an empty row of quantifiers.
bridi broda bridi naku zo'u broda

Definition	df-naku 211	Traditional definition of intuitionistic negation.
⊢ go naku zo'u broda gi ganai broda gi gai'o

Theorem	naku-uncur 212	Uncurried form of df-naku 211 (Contributed by la korvo, 20-Aug-2023.)
⊢ ganai ge naku zo'u broda gi broda gi gai'o

Theorem	lnc 213	The law of non-contradiction. No bridi is simultaneously inhabited and uninhabited. (Contributed by la korvo, 19-Sep-2024.)
⊢ naku zo'u ge naku zo'u broda gi broda

Theorem	lnci 214	The law of non-contradiction. If a bridi is simultaneously inhabited and uninhabited, then we reach an absurdity. (Contributed by la korvo, 20-Aug-2023.)
⊢ ge broda gi naku zo'u broda ⊢ gai'o

Theorem	nakui 215	Inference form of df-naku 211 (Contributed by la korvo, 9-Aug-2023.)
⊢ naku zo'u broda ⊢ ganai broda gi gai'o

Theorem	nakuii 216	Inference form of df-naku 211 (Contributed by la korvo, 9-Aug-2023.)
⊢ naku zo'u broda ⊢ broda ⊢ gai'o

Theorem	nakuri 217	Reverse inference form of df-naku 211 (Contributed by la korvo, 9-Aug-2023.)
⊢ ganai broda gi gai'o ⊢ naku zo'u broda

Theorem	na-gaiho 218	{gai'o} is uninhabited. (Contributed by la korvo, 9-Aug-2023.)
⊢ naku zo'u gai'o

Axiom	ax-sdo 219	The principle of self-defeating objects. If an object's existence would imply that it doesn't exist -- usually via contradiction -- then it doesn't exist. As a special case, if some tuple's membership in a relation would imply non-membership in that relation, then it's not a member. For a survey of this principle across maths, see [Tao]. Axiom ax-in1 in [ILE] p. 0.
⊢ ganai ganai broda gi naku zo'u broda gi naku zo'u broda

Theorem	sdoi 220	Inference form of ax-sdo 219 (Contributed by la korvo, 9-Aug-2023.)
⊢ ganai broda gi naku zo'u broda ⊢ naku zo'u broda

Axiom	ax-efq 221	The principle of explosion. If a tuple both is and is not a member of some relation, then we are inconsistent and any theorem whatsoever may be derived. The short name "efq" comes from the Latin phrase, "ex falso quodlibet".
⊢ ganai naku zo'u broda gi ganai broda gi brode

Theorem	efqi 222	Inference form of ax-efq 221 (Contributed by la korvo, 25-Jun-2024.)
⊢ naku zo'u broda ⊢ ganai broda gi brode

Theorem	efqii 223	Inference form of ax-efq 221 (Contributed by la korvo, 25-Jun-2024.)
⊢ naku zo'u broda ⊢ broda ⊢ brode

1.14 Mutual exclusion I The final of our five essential connectives. As with disjunctions, we can introduce all versions of mutual exclusion at once.

1.14.1 {gonai}

Syntax	bgon 224
bridi gonai broda gi brode

Definition	df-gonai 225	Standard constructive definition of mutual exclusion ("the exclusive OR"), based on the mnemonic given to computer scientists in the USA and UK: "It's cake or tea, but not cake and tea." Definition df-xor in [ILE] p. 0.
⊢ go gonai broda gi brode gi ge ga broda gi brode gi naku zo'u ge broda gi brode

Theorem	gonaii 226	Inference form of df-gonai 225 (Contributed by la korvo, 8-Aug-2023.)
⊢ gonai broda gi brode ⊢ ge ga broda gi brode gi naku zo'u ge broda gi brode

Theorem	gonaiil 227	Inference form of df-gonai 225 (Contributed by la korvo, 8-Aug-2023.)
⊢ gonai broda gi brode ⊢ ga broda gi brode

Theorem	gonaiir 228	Inference form of df-gonai 225 (Contributed by la korvo, 8-Aug-2023.)
⊢ gonai broda gi brode ⊢ naku zo'u ge broda gi brode

Theorem	gonairi 229	Reverse inference form of df-gonai 225 (Contributed by la korvo, 8-Aug-2023.)
⊢ ge ga broda gi brode gi naku zo'u ge broda gi brode ⊢ gonai broda gi brode

1.14.2 {.onai}

Syntax	sjonai 230
sumti ko'a .onai ko'e

Definition	df-onai 231	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 232	Inference form of df-onai 231 (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 233	Reverse inference form of df-onai 231 (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 234*
selbri bu'a jonai bu'e

Definition	df-jonai 235*	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 236*	Inference form of df-jonai 235 (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 237*	Reverse inference form of df-jonai 235 (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 238
brirebla bo'a gi'onai bo'e

Definition	df-gihonai 239	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 240	Inference form of df-gihonai 239 (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 241	Inference form of df-gihonai 239 (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 242
bridi ga broda ginai brode

Syntax	bgogin 243
bridi go broda ginai brode

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

Definition	df-ginai-go 245
⊢ 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 246
selbri cmima

Syntax	sbselcmi 247
selbri selcmi

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

2.1.2 {nomei}

Syntax	snomei 249
sumti le nomei ku

Definition	df-nomei 250	{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 zo'u ko'a cmima le nomei ku

Theorem	nomei-gaiho 251	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 252
selbri pamei

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

Theorem	pameiii 255	Inference form of df-pamei 253 (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 256	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 257
selbri gripau

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

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

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

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

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

Syntax	spk 267	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 268
selbri ckaji

Theorem	bckaji 269	{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 270	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 271	Inference form of df-ckaji 270 (Contributed by la korvo, 17-Jul-2023.)
⊢ ko'a ckaji 1 ka ce'u bo'a kei ⊢ ko'a bo'a

Theorem	ckajiri 272	Reverse inference form of df-ckaji 270 (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 273
selbri ckini

Theorem	bckini 274	{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 275
⊢ go ko'a ckini ko'e 1 ka ce'u bu'a ce'u kei gi ko'a bu'a ko'e

Theorem	ckinii 276	Inference form of df-ckini 275 (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 277	Reverse inference form of df-ckini 275 (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 278	{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 279
selbri sefsi

Definition	df-sefsi 280	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 281
selbri simsa

Theorem	bsimsa 282	{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 283	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 284	Inference form of df-simsa 283 (Contributed by la korvo, 6-Aug-2023.)
⊢ ko'a simsa ko'e ko'i ⊢ ko'a .e ko'e ckaji ko'i

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

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

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

Theorem	simsarii 288	Reverse inference form of df-simsa 283 (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 289	{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 290
selbri dunli

Theorem	bdunli 291	{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 292	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 293	Inference form of df-dunli 292 (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 294	Reverse inference form of df-dunli 292 (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 295	{dunli} is reflexive over any dunli3. (Contributed by la korvo, 14-Aug-2024.)
⊢ ko'a dunli ko'a ko'e

Theorem	dunli-sym 296	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 297
selbri mintu

Theorem	bmintu 298	{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 299	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 300	Inference form of df-mintu 299 (Contributed by la korvo, 6-Aug-2023.)
⊢ ko'a mintu ko'e ko'i ⊢ ko'a .o ko'e ckaji 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 >