P. 61 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 6001-6100   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-map 6001*	Define the mapping operation or set exponentiation. The set of all functions that map from B to A is written (A ^m B) (see mapval 6011). Many authors write A followed by B as a superscript for this operation and rely on context to avoid confusion other exponentiation operations (e.g. Definition 10.42 of [TakeutiZaring] p. 95). Other authors show B as a prefixed superscript, which is read "A pre B " (e.g. definition of [Enderton] p. 52). Definition 8.21 of [Eisenberg] p. 125 uses the notation Map(B, A) for our (A ^m B). The up-arrow is used by Donald Knuth for iterated exponentiation (Science 194, 1235-1242, 1976). We adopt the first case of his notation (simple exponentiation) and subscript it with m to distinguish it from other kinds of exponentiation. (Contributed by NM, 15-Nov-2007.)
|- ^m = (x e. _V, y e. _V |-> {f | f:y-->x})
Definition	df-pm 6002*	Define the partial mapping operation. A partial function from B to A is a function from a subset of B to A. The set of all partial functions from B to A is written (A ^pm B) (see pmvalg 6010). A notation for this operation apparently does not appear in the literature. We use ^pm to distinguish it from the less general set exponentiation operation ^m (df-map 6001) . See mapsspm 6021 for its relationship to set exponentiation. (Contributed by NM, 15-Nov-2007.)
|- ^pm = (x e. _V, y e. _V |-> {f e. ~P(y X. x) | Fun f})
Theorem	mapexi 6003*	The class of all functions mapping one set to another is a set. Remark after Definition 10.24 of [Kunen] p. 31. (Contributed by set.mm contributors, 25-Feb-2015.)
|- A e. _V   &   |- B e. _V   =>   |- {f | f:A-->B} e. _V
Theorem	mapprc 6004*	When A is a proper class, the class of all functions mapping A to B is empty. Exercise 4.41 of [Mendelson] p. 255. (Contributed by set.mm contributors, 8-Dec-2003.)
|- (-. A e. _V -> {f | f:A-->B} = (/))
Theorem	pmex 6005*	The class of all partial functions from one set to another is a set. (Contributed by set.mm contributors, 15-Nov-2007.)
|- ((A e. C /\ B e. D) -> {f | (Fun f /\ f C_ (A X. B))} e. _V)
Theorem	mapex 6006*	The class of all functions mapping one set to another is a set. Remark after Definition 10.24 of [Kunen] p. 31. (Contributed by set.mm contributors, 25-Feb-2015.)
|- ((A e. C /\ B e. D) -> {f | f:A-->B} e. _V)
Theorem	fnmap 6007	Set exponentiation has a universal domain. (Contributed by set.mm contributors, 8-Dec-2003.) (Revised by set.mm contributors, 8-Sep-2013.) (Revised by Scott Fenton, 19-Apr-2019.)
|- ^m Fn _V
Theorem	fnpm 6008	Partial function exponentiation has a universal domain. (Contributed by set.mm contributors, 14-Nov-2013.) (Revised by Scott Fenton, 19-Apr-2019.)
|- ^pm Fn _V
Theorem	mapvalg 6009*	The value of set exponentiation. (A ^m B) is the set of all functions that map from B to A. Definition 10.24 of [Kunen] p. 24. (Contributed by set.mm contributors, 8-Dec-2003.) (Revised by set.mm contributors, 8-Sep-2013.)
|- ((A e. C /\ B e. D) -> (A ^m B) = {f | f:B-->A})
Theorem	pmvalg 6010*	The value of the partial mapping operation. (A ^pm B) is the set of all partial functions that map from B to A. (Contributed by set.mm contributors, 15-Nov-2007.) (Revised by set.mm contributors, 8-Sep-2013.)
|- ((A e. C /\ B e. D) -> (A ^pm B) = {f e. ~P(B X. A) | Fun f})
Theorem	mapval 6011*	The value of set exponentiation (inference version). (A ^m B) is the set of all functions that map from B to A. Definition 10.24 of [Kunen] p. 24. (Contributed by set.mm contributors, 8-Dec-2003.)
|- A e. _V   &   |- B e. _V   =>   |- (A ^m B) = {f | f:B-->A}
Theorem	elmapg 6012	Membership relation for set exponentiation. (Contributed by set.mm contributors, 17-Oct-2006.)
|- ((A e. V /\ B e. W /\ C e. X) -> (C e. (A ^m B) <-> C:B-->A))
Theorem	elpmg 6013	The predicate "is a partial function." (Contributed by set.mm contributors, 14-Nov-2013.)
|- ((A e. V /\ B e. W /\ C e. X) -> (C e. (A ^pm B) <-> (Fun C /\ C C_ (B X. A))))
Theorem	elpm2g 6014	The predicate "is a partial function." (Contributed by set.mm contributors, 31-Dec-2013.)
|- ((A e. V /\ B e. W /\ F e. X) -> (F e. (A ^pm B) <-> (F:dom F-->A /\ dom F C_ B)))
Theorem	pmfun 6015	A partial function is a function. (Contributed by Mario Carneiro, 30-Jan-2014.)
|- (F e. (A ^pm B) -> Fun F)
Theorem	elmapi 6016	A mapping is a function, forward direction only with antecedents removed. (Contributed by set.mm contributors, 25-Feb-2015.)
|- (A e. (B ^m C) -> A:C-->B)
Theorem	elmap 6017	Membership relation for set exponentiation. (Contributed by set.mm contributors, 8-Dec-2003.)
|- A e. _V   &   |- B e. _V   &   |- F e. _V   =>   |- (F e. (A ^m B) <-> F:B-->A)
Theorem	mapval2 6018*	Alternate expression for the value of set exponentiation. (Contributed by set.mm contributors, 3-Nov-2007.)
|- A e. _V   &   |- B e. _V   &   |- F e. _V   =>   |- (A ^m B) = (~P(B X. A) i^i {f | f Fn B})
Theorem	elpm 6019	The predicate "is a partial function." (Contributed by set.mm contributors, 15-Nov-2007.) (Revised by set.mm contributors, 14-Nov-2013.)
|- A e. _V   &   |- B e. _V   &   |- F e. _V   =>   |- (F e. (A ^pm B) <-> (Fun F /\ F C_ (B X. A)))
Theorem	elpm2 6020	The predicate "is a partial function." (Contributed by set.mm contributors, 15-Nov-2007.) (Revised by set.mm contributors, 31-Dec-2013.)
|- A e. _V   &   |- B e. _V   &   |- F e. _V   =>   |- (F e. (A ^pm B) <-> (F:dom F-->A /\ dom F C_ B))
Theorem	mapsspm 6021	Set exponentiation is a subset of partial maps. (Contributed by set.mm contributors, 15-Nov-2007.)
|- (A ^m B) C_ (A ^pm B)
Theorem	mapsspw 6022	Set exponentiation is a subset of the power set of the cross product of its arguments. (Contributed by set.mm contributors, 8-Dec-2006.)
|- (A ^m B) C_ ~P(B X. A)
Theorem	map0e 6023	Set exponentiation with an empty exponent is the unit class of the empty set. (Contributed by set.mm contributors, 10-Dec-2003.)
|- A e. _V   =>   |- (A ^m (/)) = {(/)}
Theorem	map0b 6024	Set exponentiation with an empty base is the empty set, provided the exponent is nonempty. Theorem 96 of [Suppes] p. 89. (Contributed by set.mm contributors, 10-Dec-2003.) (Revised by set.mm contributors, 19-Mar-2007.)
|- A e. _V   =>   |- (A =/= (/) -> ((/) ^m A) = (/))
Theorem	map0 6025	Set exponentiation is empty iff the base is empty and the exponent is not empty. Theorem 97 of [Suppes] p. 89. (Contributed by set.mm contributors, 10-Dec-2003.) (Revised by set.mm contributors, 17-May-2007.)
|- A e. _V   &   |- B e. _V   =>   |- ((A ^m B) = (/) <-> (A = (/) /\ B =/= (/)))
Theorem	mapsn 6026*	The value of set exponentiation with a singleton exponent. Theorem 98 of [Suppes] p. 89. (Contributed by set.mm contributors, 10-Dec-2003.)
|- A e. _V   &   |- B e. _V   =>   |- (A ^m {B}) = {f | E.y e. A f = {<.B, y>.}}
Theorem	mapss 6027	Subset inheritance for set exponentiation. Theorem 99 of [Suppes] p. 89. (Contributed by set.mm contributors, 10-Dec-2003.)
|- A e. _V   &   |- B e. _V   &   |- C e. _V   =>   |- (A C_ B -> (A ^m C) C_ (B ^m C))
2.4.4  Equinumerosity
Syntax	cen 6028	Extend class definition to include the equinumerosity relation ("approximately equals" symbol)
class ~~
Definition	df-en 6029*	Define the equinumerosity relation. Definition of [Enderton] p. 129. We define ~~ to be a binary relation rather than a connective, so its arguments must be sets to be meaningful. This is acceptable because we do not consider equinumerosity for proper classes. We derive the usual definition as bren 6030. (Contributed by NM, 28-Mar-1998.)
|- ~~ = {<.x, y>. | E.f f:x-1-1-onto->y}
Theorem	bren 6030*	Equinumerosity relationship. (Contributed by SF, 23-Feb-2015.)
|- (A ~~ B <-> E.f f:A-1-1-onto->B)
Theorem	enex 6031	The equinumerosity relationship is a set. (Contributed by SF, 23-Feb-2015.)
|- ~~ e. _V
Theorem	f1oeng 6032	The domain and range of a one-to-one, onto function are equinumerous. (Contributed by SF, 23-Feb-2015.)
|- ((F e. C /\ F:A-1-1-onto->B) -> A ~~ B)
Theorem	f1oen 6033	The domain and range of a one-to-one, onto function are equinumerous. (Contributed by SF, 19-Jun-1998.)
|- F e. _V   =>   |- (F:A-1-1-onto->B -> A ~~ B)
Theorem	enrflxg 6034	Equinumerosity is reflexive. (Contributed by SF, 23-Feb-2015.)
|- (A e. V -> A ~~ A)
Theorem	enrflx 6035	Equinumerosity is reflexive. (Contributed by SF, 23-Feb-2015.)
|- A e. _V   =>   |- A ~~ A
Theorem	ensymi 6036	Equinumerosity is symmetric. (Contributed by SF, 23-Feb-2015.)
|- (A ~~ B -> B ~~ A)
Theorem	ensym 6037	Equinumerosity is symmetric. (Contributed by SF, 23-Feb-2015.)
|- (A ~~ B <-> B ~~ A)
Theorem	entr 6038	Equinumerosity is transitive. (Contributed by SF, 23-Feb-2015.)
|- ((A ~~ B /\ B ~~ C) -> A ~~ C)
Theorem	ener 6039	Equinumerosity is an equivalence relationship over the universe. (Contributed by SF, 23-Feb-2015.)
|- ~~ Er _V
Theorem	idssen 6040	Equality implies equinumerosity. (Contributed by SF, 30-Apr-1998.)
|- _I C_ ~~
Theorem	dmen 6041	The domain of equinumerosity. (Contributed by SF, 10-May-1998.)
|- dom ~~ = _V
Theorem	en0 6042	The empty set is equinumerous only to itself. Exercise 1 of [TakeutiZaring] p. 88. (Contributed by SF, 27-May-1998.)
|- (A ~~ (/) <-> A = (/))
Theorem	fundmen 6043	A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98. (Contributed by SF, 23-Feb-2015.)
|- F e. _V   =>   |- (Fun F -> dom F ~~ F)
Theorem	fundmeng 6044	A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98. (Contributed by set.mm contributors, 17-Sep-2013.)
|- ((F e. V /\ Fun F) -> dom F ~~ F)
Theorem	cnven 6045	A relational set is equinumerous to its converse. (Contributed by set.mm contributors, 28-Dec-2014.) (Modified by Scott Fenton, 17-Apr-2021.)
|- (A e. V -> A ~~ `'A)
Theorem	fndmeng 6046	A function is equinumerate to its domain. (Contributed by Paul Chapman, 22-Jun-2011.)
|- ((F Fn A /\ F e. C) -> A ~~ F)
Theorem	en2sn 6047	Two singletons are equinumerous. (Contributed by set.mm contributors, 9-Nov-2003.)
|- ((A e. C /\ B e. D) -> {A} ~~ {B})
Theorem	unen 6048	Equinumerosity of union of disjoint sets. Theorem 4 of [Suppes] p. 92. (Contributed by set.mm contributors, 11-Jun-1998.)
|- (((A ~~ B /\ C ~~ D) /\ ((A i^i C) = (/) /\ (B i^i D) = (/))) -> (A u. C) ~~ (B u. D))
Theorem	xpsnen 6049	A set is equinumerous to its cross-product with a singleton. Proposition 4.22(c) of [Mendelson] p. 254. (Contributed by set.mm contributors, 23-Feb-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (A X. {B}) ~~ A
Theorem	xpsneng 6050	A set is equinumerous to its cross-product with a singleton. Proposition 4.22(c) of [Mendelson] p. 254. (Contributed by set.mm contributors, 22-Oct-2004.)
|- ((A e. V /\ B e. W) -> (A X. {B}) ~~ A)
Theorem	endisj 6051*	Any two sets are equinumerous to disjoint sets. Exercise 4.39 of [Mendelson] p. 255. (Contributed by set.mm contributors, 16-Apr-2004.)
|- A e. _V   &   |- B e. _V   =>   |- E.xE.y((x ~~ A /\ y ~~ B) /\ (x i^i y) = (/))
Theorem	xpcomen 6052	Commutative law for equinumerosity of cross product. Proposition 4.22(d) of [Mendelson] p. 254. (Contributed by set.mm contributors, 5-Jan-2004.) (Revised by set.mm contributors, 23-Apr-2014.)
|- A e. _V   &   |- B e. _V   =>   |- (A X. B) ~~ (B X. A)
Theorem	xpcomeng 6053	Commutative law for equinumerosity of cross product. Proposition 4.22(d) of [Mendelson] p. 254. (Contributed by set.mm contributors, 27-Mar-2006.)
|- ((A e. V /\ B e. W) -> (A X. B) ~~ (B X. A))
Theorem	xpsnen2g 6054	A set is equinumerous to its cross-product with a singleton on the left. (Contributed by Stefan O'Rear, 21-Nov-2014.)
|- ((A e. V /\ B e. W) -> ({A} X. B) ~~ B)
Theorem	xpen 6055	Equinumerosity law for cross product. Proposition 4.22(b) of [Mendelson] p. 254. (Contributed by set.mm contributors, 24-Jul-2004.) (Revised by set.mm contributors, 9-Mar-2013.)
|- ((A ~~ B /\ C ~~ D) -> (A X. C) ~~ (B X. D))
Theorem	xpassenlem 6056	Lemma for xpassen 6057. Compute a projection. (Contributed by Scott Fenton, 19-Apr-2021.)
|- (y((1st o. 1st) (x) ((2nd o. 1st) (x) 2nd))x <-> ( Proj1 Proj1 y = Proj1 x /\ Proj2 Proj1 y = Proj1 Proj2 x /\ Proj2 y = Proj2 Proj2 x))
Theorem	xpassen 6057	Associative law for equinumerosity of cross product. Proposition 4.22(e) of [Mendelson] p. 254. (Contributed by SF, 24-Feb-2015.)
|- A e. _V   &   |- B e. _V   &   |- C e. _V   =>   |- ((A X. B) X. C) ~~ (A X. (B X. C))
Theorem	ensn 6058	Two singletons are equinumerous. Theorem XI.1.10 of [Rosser] p. 348. (Contributed by SF, 25-Feb-2015.)
|- A e. _V   &   |- B e. _V   =>   |- {A} ~~ {B}
Theorem	enadjlem1 6059	Lemma for enadj 6060. Calculate equality of differences. (Contributed by SF, 25-Feb-2015.)
|- (((A u. {X}) = (B u. {Y}) /\ (-. X e. A /\ -. Y e. B) /\ (Y e. A /\ X e. B)) -> (A \ {Y}) = (B \ {X}))
Theorem	enadj 6060	Equivalence law for adjunction. Theorem XI.1.13 of [Rosser] p. 348. (Contributed by SF, 25-Feb-2015.)
|- A e. _V   &   |- B e. _V   &   |- X e. _V   &   |- Y e. _V   =>   |- (((A u. {X}) = (B u. {Y}) /\ -. X e. A /\ -. Y e. B) -> A ~~ B)
Theorem	enpw1lem1 6061*	Lemma for enpw1 6062. Set up stratification for the reverse direction. (Contributed by SF, 26-Feb-2015.)
|- {<.x, y>. | {x}g{y}} e. _V
Theorem	enpw1 6062	Two classes are equinumerous iff their unit power classes are equinumerous. Theorem XI.1.33 of [Rosser] p. 368. (Contributed by SF, 26-Feb-2015.)
|- (A ~~ B <-> ~P1 A ~~ ~P1 B)
Theorem	enmap2lem1 6063*	Lemma for enmap2 6068. Set up stratification. (Contributed by SF, 26-Feb-2015.)
|- W = (s e. (G ^m A) |-> (s o. `'r))   =>   |- W e. _V
Theorem	enmap2lem2 6064*	Lemma for enmap2 6068. Establish the functionhood and domain of W. (Contributed by SF, 26-Feb-2015.)
|- W = (s e. (G ^m a) |-> (s o. `'r))   =>   |- W Fn (G ^m a)
Theorem	enmap2lem3 6065*	Lemma for enmap2 6068. Binary relationship condition over W. (Contributed by SF, 26-Feb-2015.)
|- W = (s e. (G ^m a) |-> (s o. `'r))   =>   |- (r:a-1-1-onto->b -> (SWT -> S = (T o. r)))
Theorem	enmap2lem4 6066*	Lemma for enmap2 6068. The converse of W is a function. (Contributed by SF, 26-Feb-2015.)
|- W = (s e. (G ^m a) |-> (s o. `'r))   =>   |- (r:a-1-1-onto->b -> Fun `'W)
Theorem	enmap2lem5 6067*	Lemma for enmap2 6068. Calculate the range of W. (Contributed by SF, 26-Feb-2015.)
|- W = (s e. (G ^m a) |-> (s o. `'r))   =>   |- (r:a-1-1-onto->b -> ran W = (G ^m b))
Theorem	enmap2 6068	Set exponentiation preserves equinumerosity in the second argument. Theorem XI.1.22 of [Rosser] p. 357. (Contributed by SF, 26-Feb-2015.)
|- (A ~~ B -> (C ^m A) ~~ (C ^m B))
Theorem	enmap1lem1 6069*	Lemma for enmap1 6074. Set up stratification. (Contributed by SF, 3-Mar-2015.)
|- W = (s e. (A ^m G) |-> (r o. s))   =>   |- W e. _V
Theorem	enmap1lem2 6070*	Lemma for enmap1 6074. Establish functionhood. (Contributed by SF, 3-Mar-2015.)
|- W = (s e. (A ^m G) |-> (r o. s))   =>   |- W Fn (A ^m G)
Theorem	enmap1lem3 6071*	Lemma for enmap2 6068. Binary relationship condition over W. (Contributed by SF, 3-Mar-2015.)
|- W = (s e. (A ^m G) |-> (r o. s))   =>   |- (r:A-1-1-onto->B -> (SWT -> S = (`'r o. T)))
Theorem	enmap1lem4 6072*	Lemma for enmap2 6068. The converse of W is a function. (Contributed by SF, 3-Mar-2015.)
|- W = (s e. (A ^m G) |-> (r o. s))   =>   |- (r:A-1-1-onto->B -> Fun `'W)
Theorem	enmap1lem5 6073*	Lemma for enmap2 6068. Calculate the range of W. (Contributed by SF, 3-Mar-2015.)
|- W = (s e. (A ^m G) |-> (r o. s))   =>   |- (r:A-1-1-onto->B -> ran W = (B ^m G))
Theorem	enmap1 6074	Set exponentiation preserves equinumerosity in the first argument. Theorem XI.1.23 of [Rosser] p. 357. (Contributed by SF, 3-Mar-2015.)
|- (A ~~ B -> (A ^m C) ~~ (B ^m C))
Theorem	enpw1pw 6075	Unit power class and power class commute within equivalence. Theorem XI.1.35 of [Rosser] p. 368. (Contributed by SF, 26-Feb-2015.)
|- A e. _V   =>   |- ~P1 ~PA ~~ ~P~P1 A
Theorem	enprmaplem1 6076*	Lemma for enprmap 6082. Set up stratification. (Contributed by SF, 3-Mar-2015.)
|- W = (r e. (A ^m B) |-> (`'r"{x}))   =>   |- W e. _V
Theorem	enprmaplem2 6077*	Lemma for enprmap 6082. Establish functionhood. (Contributed by SF, 3-Mar-2015.)
|- W = (r e. (A ^m B) |-> (`'r"{x}))   =>   |- W Fn (A ^m B)
Theorem	enprmaplem3 6078*	Lemma for enprmap 6082. The converse of W is a function. (Contributed by SF, 3-Mar-2015.)
|- W = (r e. (A ^m B) |-> (`'r"{x}))   =>   |- ((x =/= y /\ A = {x, y}) -> Fun `'W)
Theorem	enprmaplem4 6079*	Lemma for enprmap 6082. More stratification condition setup. (Contributed by SF, 3-Mar-2015.)
|- R = (u e. B |-> if(u e. p, x, y))   &   |- B e. _V   =>   |- R e. _V
Theorem	enprmaplem5 6080*	Lemma for enprmap 6082. Establish that ~PB is a subset of the range of W. (Contributed by SF, 3-Mar-2015.)
|- W = (r e. (A ^m B) |-> (`'r"{x}))   &   |- R = (u e. B |-> if(u e. p, x, y))   &   |- B e. _V   =>   |- ((x =/= y /\ A = {x, y}) -> ~PB C_ ran W)
Theorem	enprmaplem6 6081*	Lemma for enprmap 6082. The range of W is ~PB. (Contributed by SF, 3-Mar-2015.)
|- W = (r e. (A ^m B) |-> (`'r"{x}))   &   |- B e. _V   =>   |- ((x =/= y /\ A = {x, y}) -> ran W = ~PB)
Theorem	enprmap 6082	A mapping from a two element pair onto a set is equinumerous with the power class of the set. Theorem XI.1.28 of [Rosser] p. 360. (Contributed by SF, 3-Mar-2015.)
|- B e. _V   =>   |- ((x =/= y /\ A = {x, y}) -> (A ^m B) ~~ ~PB)
Theorem	enprmapc 6083	A mapping from a two element pair onto a set is equinumerous with the power class of the set. Theorem XI.1.28 of [Rosser] p. 360. (Contributed by SF, 3-Mar-2015.)
|- A e. _V   &   |- B e. _V   &   |- C e. _V   =>   |- ((A =/= B /\ P = {A, B}) -> (P ^m C) ~~ ~PC)
Theorem	nenpw1pwlem1 6084*	Lemma for nenpw1pw 6086. Set up stratification. (Contributed by SF, 10-Mar-2015.)
|- S = {x e. A | -. x e. (r` {x})}   =>   |- (A e. V -> S e. _V)
Theorem	nenpw1pwlem2 6085*	Lemma for nenpw1pw 6086. Establish the main theorem with an extra hypothesis. (Contributed by SF, 10-Mar-2015.)
|- S = {x e. A | -. x e. (r` {x})}   =>   |- -. ~P1 A ~~ ~PA
Theorem	nenpw1pw 6086	No unit power class is equinumerous with the corresponding power class. Theorem XI.1.6 of [Rosser] p. 347. (Contributed by SF, 10-Mar-2015.)
|- -. ~P1 A ~~ ~PA
Theorem	enpw 6087	If A and B are equinumerous, then so are their power sets. Theorem XI.1.36 of [Rosser] p. 369. (Contributed by SF, 17-Mar-2015.)
|- (A ~~ B -> ~PA ~~ ~PB)
2.4.5  Cardinal numbers
Syntax	cncs 6088	Extend the definition of a class to include the set of cardinal numbers.
class NC
Syntax	clec 6089	Extend the definition of a class to include cardinal less than or equal.
class <_c
Syntax	cltc 6090	Extend the definition of a class to include cardinal strict less than.
class <c
Syntax	cnc 6091	Extend the definition of a class to include the cardinality operation.
class Nc A
Syntax	cmuc 6092	Extend the definition of a class to include cardinal multiplication.
class ·c
Syntax	ctc 6093	Extend the definition of a class to include cardinal type raising.
class Tc A
Syntax	c2c 6094	Extend the definition of a class to include cardinal two.
class 2c
Syntax	c3c 6095	Extend the definition of a class to include cardinal three.
class 3c
Syntax	cce 6096	Extend the definition of a class to include cardinal exponentiation.
class ↑c
Syntax	ctcfn 6097	Extend the definition of a class to include the stratified T-raising function.
class TcFn
Definition	df-ncs 6098	Define the set of all cardinal numbers. We define them as equivalence classes of sets of the same size. Definition from [Rosser] p. 372. (Contributed by Scott Fenton, 24-Feb-2015.)
|- NC = (_V/. ~~ )
Definition	df-lec 6099*	Define cardinal less than or equal. Definition from [Rosser] p. 375. (Contributed by Scott Fenton, 24-Feb-2015.)
|- <_c = {<.a, b>. | E.x e. a E.y e. b x C_ y}
Definition	df-ltc 6100	Define cardinal less than. Definition from [Rosser] p. 375. (Contributed by Scott Fenton, 24-Feb-2015.)
|- <c = ( <_c \ _I )