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