P. 62 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 6101-6200   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-ltc 6101	Define cardinal less than. Definition from [Rosser] p. 375. (Contributed by Scott Fenton, 24-Feb-2015.)
⊢ <c = ( ≤c ∖ I )
Definition	df-nc 6102	Define the cardinality operation. This is the unique cardinal number containing a given set. Definition from [Rosser] p. 371. (Contributed by Scott Fenton, 24-Feb-2015.)
⊢ Nc A = [A] ≈
Definition	df-muc 6103*	Define cardinal multiplication. Definition from [Rosser] p. 378. (Contributed by Scott Fenton, 24-Feb-2015.)
⊢ ·c = (m ∈ NC , n ∈ NC ↦ {a ∣ ∃b ∈ m ∃g ∈ n a ≈ (b × g)})
Definition	df-tc 6104*	Define the type-raising operation on a cardinal number. This is the unique cardinal containing the unit power classes of the elements of the given cardinal. Definition adapted from [Rosser] p. 528. (Contributed by Scott Fenton, 24-Feb-2015.)
⊢ Tc A = (℩b(b ∈ NC ∧ ∃x ∈ A b = Nc ℘1x))
Definition	df-2c 6105	Define cardinal two. This is the set of all sets with two unique elements. (Contributed by Scott Fenton, 24-Feb-2015.)
⊢ 2c = Nc {∅, V}
Definition	df-3c 6106	Define cardinal three. This is the set of all sets with three unique elements. (Contributed by Scott Fenton, 24-Feb-2015.)
⊢ 3c = Nc {∅, V, (V ∖ {∅})}
Definition	df-ce 6107*	Define cardinal exponentiation. Definition from [Rosser] p. 381. (Contributed by Scott Fenton, 24-Feb-2015.)
⊢ ↑c = (n ∈ NC , m ∈ NC ↦ {g ∣ ∃a∃b(℘1a ∈ n ∧ ℘1b ∈ m ∧ g ≈ (a ↑m b))})
Definition	df-tcfn 6108	Define the stratified T-raising function. (Contributed by Scott Fenton, 24-Feb-2015.)
⊢ TcFn = (x ∈ 1c ↦ Tc ∪x)
Theorem	nceq 6109	Cardinality equality law. (Contributed by SF, 24-Feb-2015.)
⊢ (A = B → Nc A = Nc B)
Theorem	nceqi 6110	Equality inference for cardinality. (Contributed by SF, 24-Feb-2015.)
⊢ A = B    ⇒   ⊢ Nc A = Nc B
Theorem	nceqd 6111	Equality deduction for cardinality. (Contributed by SF, 24-Feb-2015.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → Nc A = Nc B)
Theorem	ncsex 6112	The class of all cardinal numbers is a set. (Contributed by SF, 24-Feb-2015.)
⊢ NC ∈ V
Theorem	brlecg 6113*	Binary relationship form of cardinal less than or equal. (Contributed by SF, 24-Feb-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → (A ≤c B ↔ ∃x ∈ A ∃y ∈ B x ⊆ y))
Theorem	brlec 6114*	Binary relationship form of cardinal less than or equal. (Contributed by SF, 24-Feb-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (A ≤c B ↔ ∃x ∈ A ∃y ∈ B x ⊆ y)
Theorem	brltc 6115	Binary relationship form of cardinal less than. (Contributed by SF, 4-Mar-2015.)
⊢ (A <c B ↔ (A ≤c B ∧ A ≠ B))
Theorem	lecex 6116	Cardinal less than or equal is a set. (Contributed by SF, 24-Feb-2015.)
⊢ ≤c ∈ V
Theorem	ltcex 6117	Cardinal strict less than is a set. (Contributed by SF, 24-Feb-2015.)
⊢ <c ∈ V
Theorem	ncex 6118	The cardinality of a class is a set. (Contributed by SF, 24-Feb-2015.)
⊢ Nc A ∈ V
Theorem	nulnnc 6119	The empty class is not a cardinal number. (Contributed by SF, 24-Feb-2015.)
⊢ ¬ ∅ ∈ NC
Theorem	elncs 6120*	Membership in the cardinals. (Contributed by SF, 24-Feb-2015.)
⊢ (A ∈ NC ↔ ∃x A = Nc x)
Theorem	ncelncs 6121	The cardinality of a set is a cardinal number. (Contributed by SF, 24-Feb-2015.)
⊢ (A ∈ V → Nc A ∈ NC )
Theorem	ncelncsi 6122	The cardinality of a set is a cardinal number. (Contributed by SF, 10-Mar-2015.)
⊢ A ∈ V    ⇒   ⊢ Nc A ∈ NC
Theorem	ncidg 6123	A set is a member of its own cardinal. (Contributed by SF, 24-Feb-2015.)
⊢ (A ∈ V → A ∈ Nc A)
Theorem	ncid 6124	A set is a member of its own cardinal. (Contributed by SF, 24-Feb-2015.)
⊢ A ∈ V    ⇒   ⊢ A ∈ Nc A
Theorem	ncprc 6125	The cardinality of a proper class is the empty set. (Contributed by SF, 24-Feb-2015.)
⊢ (¬ A ∈ V → Nc A = ∅)
Theorem	elnc 6126	Membership in cardinality. (Contributed by SF, 24-Feb-2015.)
⊢ (A ∈ Nc B ↔ A ≈ B)
Theorem	eqncg 6127	Equality of cardinalities. (Contributed by SF, 24-Feb-2015.)
⊢ (A ∈ V → ( Nc A = Nc B ↔ A ≈ B))
Theorem	eqnc 6128	Equality of cardinalities. (Contributed by SF, 24-Feb-2015.)
⊢ A ∈ V    ⇒   ⊢ ( Nc A = Nc B ↔ A ≈ B)
Theorem	ncseqnc 6129	A cardinal is equal to the cardinality of a set iff it contains the set. (Contributed by SF, 24-Feb-2015.)
⊢ (A ∈ NC → (A = Nc X ↔ X ∈ A))
Theorem	eqnc2 6130	Alternate condition for equality to a cardinality. (Contributed by SF, 18-Mar-2015.)
⊢ X ∈ V    ⇒   ⊢ (A = Nc X ↔ (A ∈ NC ∧ X ∈ A))
Theorem	ovmuc 6131*	The value of cardinal multiplication. (Contributed by SF, 10-Mar-2015.)
⊢ ((M ∈ NC ∧ N ∈ NC ) → (M ·c N) = {a ∣ ∃b ∈ M ∃g ∈ N a ≈ (b × g)})
Theorem	mucnc 6132	Cardinal multiplication in terms of cardinality. Theorem XI.2.27 of [Rosser] p. 378. (Contributed by SF, 10-Mar-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ( Nc A ·c Nc B) = Nc (A × B)
Theorem	muccl 6133	Closure law for cardinal multiplication. (Contributed by SF, 10-Mar-2015.)
⊢ ((A ∈ NC ∧ B ∈ NC ) → (A ·c B) ∈ NC )
Theorem	mucex 6134	Cardinal multiplication is a set. (Contributed by SF, 24-Feb-2015.)
⊢ ·c ∈ V
Theorem	muccom 6135	Cardinal multiplication commutes. Theorem XI.2.28 of [Rosser] p. 378. (Contributed by SF, 10-Mar-2015.)
⊢ ((A ∈ NC ∧ B ∈ NC ) → (A ·c B) = (B ·c A))
Theorem	mucass 6136	Cardinal multiplication associates. Theorem XI.2.29 of [Rosser] p. 378. (Contributed by SF, 10-Mar-2015.)
⊢ ((A ∈ NC ∧ B ∈ NC ∧ C ∈ NC ) → ((A ·c B) ·c C) = (A ·c (B ·c C)))
Theorem	ncdisjun 6137	Cardinality of disjoint union of two sets. (Contributed by SF, 24-Feb-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ((A ∩ B) = ∅ → Nc (A ∪ B) = ( Nc A +c Nc B))
Theorem	df0c2 6138	Cardinal zero is the cardinality of the empty set. Theorem XI.2.7 of [Rosser] p. 372. (Contributed by SF, 24-Feb-2015.)
⊢ 0c = Nc ∅
Theorem	0cnc 6139	Cardinal zero is a cardinal number. Corollary 1 to theorem XI.2.7 of [Rosser] p. 373. (Contributed by SF, 24-Feb-2015.)
⊢ 0c ∈ NC
Theorem	1cnc 6140	Cardinal one is a cardinal number. Corollary 2 to theorem XI.2.8 of [Rosser] p. 373. (Contributed by SF, 24-Feb-2015.)
⊢ 1c ∈ NC
Theorem	df1c3 6141	Cardinal one is the cardinality of a singleton. Theorem XI.2.8 of [Rosser] p. 373. (Contributed by SF, 2-Mar-2015.)
⊢ A ∈ V    ⇒   ⊢ 1c = Nc {A}
Theorem	df1c3g 6142	Cardinal one is the cardinality of a singleton. Theorem XI.2.8 of [Rosser] p. 373. (Contributed by SF, 13-Mar-2015.)
⊢ (A ∈ V → 1c = Nc {A})
Theorem	muc0 6143	Cardinal multiplication by zero. Theorem XI.2.32 of [Rosser] p. 379. (Contributed by SF, 10-Mar-2015.)
⊢ (A ∈ NC → (A ·c 0c) = 0c)
Theorem	mucid1 6144	Cardinal multiplication by one. (Contributed by SF, 11-Mar-2015.)
⊢ (A ∈ NC → (A ·c 1c) = A)
Theorem	ncaddccl 6145	The cardinals are closed under cardinal addition. Theorem XI.2.10 of [Rosser] p. 374. (Contributed by SF, 24-Feb-2015.)
⊢ ((A ∈ NC ∧ B ∈ NC ) → (A +c B) ∈ NC )
Theorem	peano2nc 6146	The successor of a cardinal is a cardinal. (Contributed by SF, 24-Feb-2015.)
⊢ (A ∈ NC → (A +c 1c) ∈ NC )
Theorem	nnnc 6147	A finite cardinal number is a cardinal number. (Contributed by SF, 24-Feb-2015.)
⊢ (A ∈ Nn → A ∈ NC )
Theorem	nnssnc 6148	The finite cardinals are a subset of the cardinals. Theorem XI.2.11 of [Rosser] p. 374. (Contributed by SF, 24-Feb-2015.)
⊢ Nn ⊆ NC
Theorem	ncdisjeq 6149	Two cardinals are either disjoint or equal. (Contributed by SF, 25-Feb-2015.)
⊢ ((A ∈ NC ∧ B ∈ NC ) → ((A ∩ B) = ∅ ∨ A = B))
Theorem	nceleq 6150	If two cardinals have an element in common, then they are equal. (Contributed by SF, 25-Feb-2015.)
⊢ (((A ∈ NC ∧ B ∈ NC ) ∧ (X ∈ A ∧ X ∈ B)) → A = B)
Theorem	peano4nc 6151	Successor is one-to-one over the cardinals. Theorem XI.2.12 of [Rosser] p. 375. (Contributed by SF, 25-Feb-2015.)
⊢ ((A ∈ NC ∧ B ∈ NC ) → ((A +c 1c) = (B +c 1c) ↔ A = B))
Theorem	ncssfin 6152	A cardinal is finite iff it is a subset of Fin. (Contributed by SF, 25-Feb-2015.)
⊢ (A ∈ NC → (A ∈ Nn ↔ A ⊆ Fin ))
Theorem	ncpw1 6153	The cardinality of two sets are equal iff their unit power classes have the same cardinality. (Contributed by SF, 25-Feb-2015.)
⊢ A ∈ V    ⇒   ⊢ ( Nc A = Nc B ↔ Nc ℘1A = Nc ℘1B)
Theorem	ncpwpw1 6154	Power class and unit power class commute within cardinality. (Contributed by SF, 26-Feb-2015.)
⊢ A ∈ V    ⇒   ⊢ Nc ℘℘1A = Nc ℘1℘A
Theorem	ncpw1c 6155	The cardinality of 1c is equal to that of its power class. (Contributed by SF, 26-Feb-2015.)
⊢ Nc ℘1c = Nc 1c
Theorem	1p1e2c 6156	One plus one equals two. Theorem *110.64 of [WhiteheadRussell] p. 86. This theorem is occasionally useful. (Contributed by SF, 2-Mar-2015.)
⊢ (1c +c 1c) = 2c
Theorem	2p1e3c 6157	Two plus one equals three. (Contributed by SF, 2-Mar-2015.)
⊢ (2c +c 1c) = 3c
Theorem	tcex 6158	The cardinal T operation always yields a set. (Contributed by SF, 2-Mar-2015.)
⊢ Tc A ∈ V
Theorem	tceq 6159	Equality theorem for cardinal T operator. (Contributed by SF, 2-Mar-2015.)
⊢ (A = B → Tc A = Tc B)
Theorem	ncspw1eu 6160*	Given a cardinal, there is a unique cardinal that contains the unit power class of its members. (Contributed by SF, 2-Mar-2015.)
⊢ (A ∈ NC → ∃!x ∈ NC ∃y ∈ A x = Nc ℘1y)
Theorem	tccl 6161	The cardinal T operation over a cardinal yields a cardinal. (Contributed by SF, 2-Mar-2015.)
⊢ (A ∈ NC → Tc A ∈ NC )
Theorem	eqtc 6162*	The defining property of the cardinal T operation. (Contributed by SF, 2-Mar-2015.)
⊢ (A ∈ NC → ( Tc A = B ↔ ∃x ∈ A B = Nc ℘1x))
Theorem	pw1eltc 6163	The unit power class of an element of a cardinal is in the cardinal's T raising. (Contributed by SF, 2-Mar-2015.)
⊢ ((A ∈ NC ∧ B ∈ A) → ℘1B ∈ Tc A)
Theorem	tc0c 6164	The T raising of cardinal zero is still cardinal zero. (Contributed by SF, 2-Mar-2015.)
⊢ Tc 0c = 0c
Theorem	tcdi 6165	T raising distributes over addition. (Contributed by SF, 2-Mar-2015.)
⊢ ((A ∈ NC ∧ B ∈ NC ) → Tc (A +c B) = ( Tc A +c Tc B))
Theorem	tc1c 6166	T raising does not change cardinal one. (Contributed by SF, 2-Mar-2015.)
⊢ Tc 1c = 1c
Theorem	tc2c 6167	T raising does not change cardinal two. (Contributed by SF, 2-Mar-2015.)
⊢ Tc 2c = 2c
Theorem	2nnc 6168	Two is a finite cardinal. (Contributed by SF, 4-Mar-2015.)
⊢ 2c ∈ Nn
Theorem	2nc 6169	Two is a cardinal number. (Contributed by SF, 3-Mar-2015.)
⊢ 2c ∈ NC
Theorem	pw1fin 6170	The unit power class of a finite set is finite. (Contributed by SF, 3-Mar-2015.)
⊢ (A ∈ Fin → ℘1A ∈ Fin )
Theorem	nntccl 6171	Cardinal T is closed under the natural numbers. (Contributed by SF, 3-Mar-2015.)
⊢ (A ∈ Nn → Tc A ∈ Nn )
Theorem	ovcelem1 6172*	Lemma for ovce 6173. Set up stratification for the result. (Contributed by SF, 6-Mar-2015.)
⊢ ((N ∈ V ∧ M ∈ W) → {g ∣ ∃a∃b(℘1a ∈ N ∧ ℘1b ∈ M ∧ g ≈ (a ↑m b))} ∈ V)
Theorem	ovce 6173*	The value of cardinal exponentiation. (Contributed by SF, 3-Mar-2015.)
⊢ ((N ∈ NC ∧ M ∈ NC ) → (N ↑c M) = {g ∣ ∃a∃b(℘1a ∈ N ∧ ℘1b ∈ M ∧ g ≈ (a ↑m b))})
Theorem	ceexlem1 6174*	Lemma for ceex 6175. Set up part of the stratification. (Contributed by SF, 6-Mar-2015.)
⊢ (⟨{{a}}, n⟩ ∈ ( S ∘ SI Pw1Fn ) ↔ ℘1a ∈ n)
Theorem	ceex 6175	Cardinal exponentiation is stratified. (Contributed by SF, 3-Mar-2015.)
⊢ ↑c ∈ V
Theorem	elce 6176*	Membership in cardinal exponentiation. Theorem XI.2.38 of [Rosser] p. 382. (Contributed by SF, 6-Mar-2015.)
⊢ ((N ∈ NC ∧ M ∈ NC ) → (A ∈ (N ↑c M) ↔ ∃x∃y(℘1x ∈ N ∧ ℘1y ∈ M ∧ A ≈ (x ↑m y))))
Theorem	fnce 6177	Functionhood statement for cardinal exponentiation. (Contributed by SF, 6-Mar-2015.)
⊢ ↑c Fn ( NC × NC )
Theorem	ce0nnul 6178*	A condition for cardinal exponentiation being nonempty. Theorem XI.2.42 of [Rosser] p. 382. (Contributed by SF, 6-Mar-2015.)
⊢ (M ∈ NC → ((M ↑c 0c) ≠ ∅ ↔ ∃a℘1a ∈ M))
Theorem	ce0nnuli 6179	Inference form of ce0nnul 6178. (Contributed by SF, 9-Mar-2015.)
⊢ ((M ∈ NC ∧ ℘1A ∈ M) → (M ↑c 0c) ≠ ∅)
Theorem	ce0addcnnul 6180	The sum of two cardinals raised to 0c is nonempty iff each addend raised to 0c is nonempty. Theorem XI.2.43 of [Rosser] p. 383. (Contributed by SF, 9-Mar-2015.)
⊢ ((M ∈ NC ∧ N ∈ NC ) → (((M +c N) ↑c 0c) ≠ ∅ ↔ ((M ↑c 0c) ≠ ∅ ∧ (N ↑c 0c) ≠ ∅)))
Theorem	ce0nn 6181	A natural raised to cardinal zero is nonempty. Theorem XI.2.44 of [Rosser] p. 383. (Contributed by SF, 9-Mar-2015.)
⊢ (N ∈ Nn → (N ↑c 0c) ≠ ∅)
Theorem	cenc 6182	Cardinal exponentiation in terms of cardinality. Theorem XI.2.39 of [Rosser] p. 382. (Contributed by SF, 6-Mar-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ( Nc ℘1A ↑c Nc ℘1B) = Nc (A ↑m B)
Theorem	ce0nnulb 6183	Cardinal exponentiation is nonempty iff the two sets raised to zero are nonempty. Theorem XI.2.47 of [Rosser] p. 384. (Contributed by SF, 9-Mar-2015.)
⊢ ((N ∈ NC ∧ M ∈ NC ) → (((N ↑c 0c) ≠ ∅ ∧ (M ↑c 0c) ≠ ∅) ↔ (N ↑c M) ≠ ∅))
Theorem	ceclb 6184	Biconditional closure law for cardinal exponentiation. Theorem XI.2.48 of [Rosser] p. 384. (Contributed by SF, 9-Mar-2015.)
⊢ ((M ∈ NC ∧ N ∈ NC ) → (((M ↑c 0c) ≠ ∅ ∧ (N ↑c 0c) ≠ ∅) ↔ (M ↑c N) ∈ NC ))
Theorem	ce0nulnc 6185	Cardinal exponentiation to zero is a cardinal iff it is nonempty. Corollary 1 of theorem XI.2.38 of [Rosser] p. 384. (Contributed by SF, 13-Mar-2015.)
⊢ (M ∈ NC → ((M ↑c 0c) ≠ ∅ ↔ (M ↑c 0c) ∈ NC ))
Theorem	ce0ncpw1 6186*	If cardinal exponentiation to zero is a cardinal, then the base is the cardinality of some unit power class. Corollary 2 of theorem XI.2.48 of [Rosser] p. 384. (Contributed by SF, 9-Mar-2015.)
⊢ ((M ∈ NC ∧ (M ↑c 0c) ∈ NC ) → ∃a M = Nc ℘1a)
Theorem	cecl 6187	Closure law for cardinal exponentiation. Corollary 3 of theorem XI.2.48 of [Rosser] p. 384. (Contributed by SF, 9-Mar-2015.)
⊢ (((M ∈ NC ∧ N ∈ NC ) ∧ ((M ↑c 0c) ∈ NC ∧ (N ↑c 0c) ∈ NC )) → (M ↑c N) ∈ NC )
Theorem	ceclr 6188	Reverse closure law for cardinal exponentiation. (Contributed by SF, 13-Mar-2015.)
⊢ ((M ∈ NC ∧ N ∈ NC ∧ (M ↑c N) ∈ NC ) → ((M ↑c 0c) ∈ NC ∧ (N ↑c 0c) ∈ NC ))
Theorem	fce 6189	Full functionhood statement for cardinal exponentiation. (Contributed by SF, 13-Mar-2015.)
⊢ ↑c :( NC × NC )–→( NC ∪ {∅})
Theorem	ceclnn1 6190	Closure law for cardinal exponentiation when the base is a natural. (Contributed by SF, 13-Mar-2015.)
⊢ ((M ∈ Nn ∧ N ∈ NC ∧ (N ↑c 0c) ∈ NC ) → (M ↑c N) ∈ NC )
Theorem	ce0 6191	The value of nonempty cardinal exponentiation. Theorem XI.2.49 of [Rosser] p. 385. (Contributed by SF, 9-Mar-2015.)
⊢ ((M ∈ NC ∧ (M ↑c 0c) ∈ NC ) → (M ↑c 0c) = 1c)
Theorem	el2c 6192*	Membership in cardinal two. (Contributed by SF, 3-Mar-2015.)
⊢ (A ∈ 2c ↔ ∃x∃y(x ≠ y ∧ A = {x, y}))
Theorem	ce2 6193	The value of base two cardinal exponentiation. Theorem XI.2.70 of [Rosser] p. 389. (Contributed by SF, 3-Mar-2015.)
⊢ A ∈ V    ⇒   ⊢ (M = Nc ℘1A → (2c ↑c M) = Nc ℘A)
Theorem	ce2nc1 6194	Compute an exponent of the cardinality of one. Theorem 4.3 of [Specker] p. 973. (Contributed by SF, 4-Mar-2015.)
⊢ (2c ↑c Nc 1c) = Nc V
Theorem	ce2ncpw11c 6195	Compute an exponent of the cardinality of the unit power class of one. Theorem 4.4 of [Specker] p. 973. (Contributed by SF, 4-Mar-2015.)
⊢ (2c ↑c Nc ℘11c) = Nc 1c
Theorem	nclec 6196	A relationship between cardinality, subset, and cardinal less than. (Contributed by SF, 17-Mar-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (A ⊆ B → Nc A ≤c Nc B)
Theorem	lecidg 6197	A nonempty set is less than or equal to itself. Theorem XI.2.14 of [Rosser] p. 375. (Contributed by SF, 4-Mar-2015.)
⊢ ((A ∈ V ∧ A ≠ ∅) → A ≤c A)
Theorem	nclecid 6198	A cardinal is less than or equal to itself. Corollary 1 of theorem XI.2.14 of [Rosser] p. 376. (Contributed by SF, 4-Mar-2015.)
⊢ (A ∈ NC → A ≤c A)
Theorem	lec0cg 6199	Cardinal zero is a minimal element of cardinal less than or equal. Theorem XI.2.15 of [Rosser] p. 376. (Contributed by SF, 4-Mar-2015.)
⊢ ((A ∈ V ∧ A ≠ ∅) → 0c ≤c A)
Theorem	lecncvg 6200	The cardinality of V is a maximal element of cardinal less than or equal. Theorem XI.2.16 of [Rosser] p. 376. (Contributed by SF, 4-Mar-2015.)
⊢ ((A ∈ V ∧ A ≠ ∅) → A ≤c Nc V)