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
Syntax	cpm 6001	Extend the definition of a class to include the partial mapping operation. (Read for A ↑m B, "the set of all partial functions that map from B to A.)
class ↑pm
Definition	df-map 6002*	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 6012). 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 ∈ V, y ∈ V ↦ {f ∣ f:y–→x})
Definition	df-pm 6003*	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 6011). 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 6002) . See mapsspm 6022 for its relationship to set exponentiation. (Contributed by NM, 15-Nov-2007.)
⊢ ↑pm = (x ∈ V, y ∈ V ↦ {f ∈ ℘(y × x) ∣ Fun f})
Theorem	mapexi 6004*	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 ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ {f ∣ f:A–→B} ∈ V
Theorem	mapprc 6005*	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 ∈ V → {f ∣ f:A–→B} = ∅)
Theorem	pmex 6006*	The class of all partial functions from one set to another is a set. (Contributed by set.mm contributors, 15-Nov-2007.)
⊢ ((A ∈ C ∧ B ∈ D) → {f ∣ (Fun f ∧ f ⊆ (A × B))} ∈ V)
Theorem	mapex 6007*	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 ∈ C ∧ B ∈ D) → {f ∣ f:A–→B} ∈ V)
Theorem	fnmap 6008	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 6009	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 6010*	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 ∈ C ∧ B ∈ D) → (A ↑m B) = {f ∣ f:B–→A})
Theorem	pmvalg 6011*	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 ∈ C ∧ B ∈ D) → (A ↑pm B) = {f ∈ ℘(B × A) ∣ Fun f})
Theorem	mapval 6012*	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 ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (A ↑m B) = {f ∣ f:B–→A}
Theorem	elmapg 6013	Membership relation for set exponentiation. (Contributed by set.mm contributors, 17-Oct-2006.)
⊢ ((A ∈ V ∧ B ∈ W ∧ C ∈ X) → (C ∈ (A ↑m B) ↔ C:B–→A))
Theorem	elpmg 6014	The predicate "is a partial function." (Contributed by set.mm contributors, 14-Nov-2013.)
⊢ ((A ∈ V ∧ B ∈ W ∧ C ∈ X) → (C ∈ (A ↑pm B) ↔ (Fun C ∧ C ⊆ (B × A))))
Theorem	elpm2g 6015	The predicate "is a partial function." (Contributed by set.mm contributors, 31-Dec-2013.)
⊢ ((A ∈ V ∧ B ∈ W ∧ F ∈ X) → (F ∈ (A ↑pm B) ↔ (F:dom F–→A ∧ dom F ⊆ B)))
Theorem	pmfun 6016	A partial function is a function. (Contributed by Mario Carneiro, 30-Jan-2014.)
⊢ (F ∈ (A ↑pm B) → Fun F)
Theorem	elmapi 6017	A mapping is a function, forward direction only with antecedents removed. (Contributed by set.mm contributors, 25-Feb-2015.)
⊢ (A ∈ (B ↑m C) → A:C–→B)
Theorem	elmap 6018	Membership relation for set exponentiation. (Contributed by set.mm contributors, 8-Dec-2003.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ F ∈ V    ⇒   ⊢ (F ∈ (A ↑m B) ↔ F:B–→A)
Theorem	mapval2 6019*	Alternate expression for the value of set exponentiation. (Contributed by set.mm contributors, 3-Nov-2007.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ F ∈ V    ⇒   ⊢ (A ↑m B) = (℘(B × A) ∩ {f ∣ f Fn B})
Theorem	elpm 6020	The predicate "is a partial function." (Contributed by set.mm contributors, 15-Nov-2007.) (Revised by set.mm contributors, 14-Nov-2013.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ F ∈ V    ⇒   ⊢ (F ∈ (A ↑pm B) ↔ (Fun F ∧ F ⊆ (B × A)))
Theorem	elpm2 6021	The predicate "is a partial function." (Contributed by set.mm contributors, 15-Nov-2007.) (Revised by set.mm contributors, 31-Dec-2013.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ F ∈ V    ⇒   ⊢ (F ∈ (A ↑pm B) ↔ (F:dom F–→A ∧ dom F ⊆ B))
Theorem	mapsspm 6022	Set exponentiation is a subset of partial maps. (Contributed by set.mm contributors, 15-Nov-2007.)
⊢ (A ↑m B) ⊆ (A ↑pm B)
Theorem	mapsspw 6023	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) ⊆ ℘(B × A)
Theorem	map0e 6024	Set exponentiation with an empty exponent is the unit class of the empty set. (Contributed by set.mm contributors, 10-Dec-2003.)
⊢ A ∈ V    ⇒   ⊢ (A ↑m ∅) = {∅}
Theorem	map0b 6025	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 ∈ V    ⇒   ⊢ (A ≠ ∅ → (∅ ↑m A) = ∅)
Theorem	map0 6026	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 ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ((A ↑m B) = ∅ ↔ (A = ∅ ∧ B ≠ ∅))
Theorem	mapsn 6027*	The value of set exponentiation with a singleton exponent. Theorem 98 of [Suppes] p. 89. (Contributed by set.mm contributors, 10-Dec-2003.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (A ↑m {B}) = {f ∣ ∃y ∈ A f = {⟨B, y⟩}}
Theorem	mapss 6028	Subset inheritance for set exponentiation. Theorem 99 of [Suppes] p. 89. (Contributed by set.mm contributors, 10-Dec-2003.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    ⇒   ⊢ (A ⊆ B → (A ↑m C) ⊆ (B ↑m C))
2.4.4  Equinumerosity
Syntax	cen 6029	Extend class definition to include the equinumerosity relation ("approximately equals" symbol)
class ≈
Definition	df-en 6030*	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 6031. (Contributed by NM, 28-Mar-1998.)
⊢ ≈ = {⟨x, y⟩ ∣ ∃f f:x–1-1-onto→y}
Theorem	bren 6031*	Equinumerosity relationship. (Contributed by SF, 23-Feb-2015.)
⊢ (A ≈ B ↔ ∃f f:A–1-1-onto→B)
Theorem	enex 6032	The equinumerosity relationship is a set. (Contributed by SF, 23-Feb-2015.)
⊢ ≈ ∈ V
Theorem	f1oeng 6033	The domain and range of a one-to-one, onto function are equinumerous. (Contributed by SF, 23-Feb-2015.)
⊢ ((F ∈ C ∧ F:A–1-1-onto→B) → A ≈ B)
Theorem	f1oen 6034	The domain and range of a one-to-one, onto function are equinumerous. (Contributed by SF, 19-Jun-1998.)
⊢ F ∈ V    ⇒   ⊢ (F:A–1-1-onto→B → A ≈ B)
Theorem	enrflxg 6035	Equinumerosity is reflexive. (Contributed by SF, 23-Feb-2015.)
⊢ (A ∈ V → A ≈ A)
Theorem	enrflx 6036	Equinumerosity is reflexive. (Contributed by SF, 23-Feb-2015.)
⊢ A ∈ V    ⇒   ⊢ A ≈ A
Theorem	ensymi 6037	Equinumerosity is symmetric. (Contributed by SF, 23-Feb-2015.)
⊢ (A ≈ B → B ≈ A)
Theorem	ensym 6038	Equinumerosity is symmetric. (Contributed by SF, 23-Feb-2015.)
⊢ (A ≈ B ↔ B ≈ A)
Theorem	entr 6039	Equinumerosity is transitive. (Contributed by SF, 23-Feb-2015.)
⊢ ((A ≈ B ∧ B ≈ C) → A ≈ C)
Theorem	ener 6040	Equinumerosity is an equivalence relationship over the universe. (Contributed by SF, 23-Feb-2015.)
⊢ ≈ Er V
Theorem	idssen 6041	Equality implies equinumerosity. (Contributed by SF, 30-Apr-1998.)
⊢ I ⊆ ≈
Theorem	dmen 6042	The domain of equinumerosity. (Contributed by SF, 10-May-1998.)
⊢ dom ≈ = V
Theorem	en0 6043	The empty set is equinumerous only to itself. Exercise 1 of [TakeutiZaring] p. 88. (Contributed by SF, 27-May-1998.)
⊢ (A ≈ ∅ ↔ A = ∅)
Theorem	fundmen 6044	A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98. (Contributed by SF, 23-Feb-2015.)
⊢ F ∈ V    ⇒   ⊢ (Fun F → dom F ≈ F)
Theorem	fundmeng 6045	A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98. (Contributed by set.mm contributors, 17-Sep-2013.)
⊢ ((F ∈ V ∧ Fun F) → dom F ≈ F)
Theorem	cnven 6046	A relational set is equinumerous to its converse. (Contributed by set.mm contributors, 28-Dec-2014.) (Modified by Scott Fenton, 17-Apr-2021.)
⊢ (A ∈ V → A ≈ ◡A)
Theorem	fndmeng 6047	A function is equinumerate to its domain. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ ((F Fn A ∧ F ∈ C) → A ≈ F)
Theorem	en2sn 6048	Two singletons are equinumerous. (Contributed by set.mm contributors, 9-Nov-2003.)
⊢ ((A ∈ C ∧ B ∈ D) → {A} ≈ {B})
Theorem	unen 6049	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 ∩ C) = ∅ ∧ (B ∩ D) = ∅)) → (A ∪ C) ≈ (B ∪ D))
Theorem	xpsnen 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, 23-Feb-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (A × {B}) ≈ A
Theorem	xpsneng 6051	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 ∈ V ∧ B ∈ W) → (A × {B}) ≈ A)
Theorem	endisj 6052*	Any two sets are equinumerous to disjoint sets. Exercise 4.39 of [Mendelson] p. 255. (Contributed by set.mm contributors, 16-Apr-2004.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ∃x∃y((x ≈ A ∧ y ≈ B) ∧ (x ∩ y) = ∅)
Theorem	xpcomen 6053	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 ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (A × B) ≈ (B × A)
Theorem	xpcomeng 6054	Commutative law for equinumerosity of cross product. Proposition 4.22(d) of [Mendelson] p. 254. (Contributed by set.mm contributors, 27-Mar-2006.)
⊢ ((A ∈ V ∧ B ∈ W) → (A × B) ≈ (B × A))
Theorem	xpsnen2g 6055	A set is equinumerous to its cross-product with a singleton on the left. (Contributed by Stefan O'Rear, 21-Nov-2014.)
⊢ ((A ∈ V ∧ B ∈ W) → ({A} × B) ≈ B)
Theorem	xpen 6056	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 × C) ≈ (B × D))
Theorem	xpassenlem 6057	Lemma for xpassen 6058. Compute a projection. (Contributed by Scott Fenton, 19-Apr-2021.)
⊢ (y((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))x ↔ ( Proj1 Proj1 y = Proj1 x ∧ Proj2 Proj1 y = Proj1 Proj2 x ∧ Proj2 y = Proj2 Proj2 x))
Theorem	xpassen 6058	Associative law for equinumerosity of cross product. Proposition 4.22(e) of [Mendelson] p. 254. (Contributed by SF, 24-Feb-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    ⇒   ⊢ ((A × B) × C) ≈ (A × (B × C))
Theorem	ensn 6059	Two singletons are equinumerous. Theorem XI.1.10 of [Rosser] p. 348. (Contributed by SF, 25-Feb-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ {A} ≈ {B}
Theorem	enadjlem1 6060	Lemma for enadj 6061. Calculate equality of differences. (Contributed by SF, 25-Feb-2015.)
⊢ (((A ∪ {X}) = (B ∪ {Y}) ∧ (¬ X ∈ A ∧ ¬ Y ∈ B) ∧ (Y ∈ A ∧ X ∈ B)) → (A ∖ {Y}) = (B ∖ {X}))
Theorem	enadj 6061	Equivalence law for adjunction. Theorem XI.1.13 of [Rosser] p. 348. (Contributed by SF, 25-Feb-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ X ∈ V    &   ⊢ Y ∈ V    ⇒   ⊢ (((A ∪ {X}) = (B ∪ {Y}) ∧ ¬ X ∈ A ∧ ¬ Y ∈ B) → A ≈ B)
Theorem	enpw1lem1 6062*	Lemma for enpw1 6063. Set up stratification for the reverse direction. (Contributed by SF, 26-Feb-2015.)
⊢ {⟨x, y⟩ ∣ {x}g{y}} ∈ V
Theorem	enpw1 6063	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 ↔ ℘1A ≈ ℘1B)
Theorem	enmap2lem1 6064*	Lemma for enmap2 6069. Set up stratification. (Contributed by SF, 26-Feb-2015.)
⊢ W = (s ∈ (G ↑m A) ↦ (s ∘ ◡r))    ⇒   ⊢ W ∈ V
Theorem	enmap2lem2 6065*	Lemma for enmap2 6069. Establish the functionhood and domain of W. (Contributed by SF, 26-Feb-2015.)
⊢ W = (s ∈ (G ↑m a) ↦ (s ∘ ◡r))    ⇒   ⊢ W Fn (G ↑m a)
Theorem	enmap2lem3 6066*	Lemma for enmap2 6069. Binary relationship condition over W. (Contributed by SF, 26-Feb-2015.)
⊢ W = (s ∈ (G ↑m a) ↦ (s ∘ ◡r))    ⇒   ⊢ (r:a–1-1-onto→b → (SWT → S = (T ∘ r)))
Theorem	enmap2lem4 6067*	Lemma for enmap2 6069. The converse of W is a function. (Contributed by SF, 26-Feb-2015.)
⊢ W = (s ∈ (G ↑m a) ↦ (s ∘ ◡r))    ⇒   ⊢ (r:a–1-1-onto→b → Fun ◡W)
Theorem	enmap2lem5 6068*	Lemma for enmap2 6069. Calculate the range of W. (Contributed by SF, 26-Feb-2015.)
⊢ W = (s ∈ (G ↑m a) ↦ (s ∘ ◡r))    ⇒   ⊢ (r:a–1-1-onto→b → ran W = (G ↑m b))
Theorem	enmap2 6069	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 6070*	Lemma for enmap1 6075. Set up stratification. (Contributed by SF, 3-Mar-2015.)
⊢ W = (s ∈ (A ↑m G) ↦ (r ∘ s))    ⇒   ⊢ W ∈ V
Theorem	enmap1lem2 6071*	Lemma for enmap1 6075. Establish functionhood. (Contributed by SF, 3-Mar-2015.)
⊢ W = (s ∈ (A ↑m G) ↦ (r ∘ s))    ⇒   ⊢ W Fn (A ↑m G)
Theorem	enmap1lem3 6072*	Lemma for enmap2 6069. Binary relationship condition over W. (Contributed by SF, 3-Mar-2015.)
⊢ W = (s ∈ (A ↑m G) ↦ (r ∘ s))    ⇒   ⊢ (r:A–1-1-onto→B → (SWT → S = (◡r ∘ T)))
Theorem	enmap1lem4 6073*	Lemma for enmap2 6069. The converse of W is a function. (Contributed by SF, 3-Mar-2015.)
⊢ W = (s ∈ (A ↑m G) ↦ (r ∘ s))    ⇒   ⊢ (r:A–1-1-onto→B → Fun ◡W)
Theorem	enmap1lem5 6074*	Lemma for enmap2 6069. Calculate the range of W. (Contributed by SF, 3-Mar-2015.)
⊢ W = (s ∈ (A ↑m G) ↦ (r ∘ s))    ⇒   ⊢ (r:A–1-1-onto→B → ran W = (B ↑m G))
Theorem	enmap1 6075	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 6076	Unit power class and power class commute within equivalence. Theorem XI.1.35 of [Rosser] p. 368. (Contributed by SF, 26-Feb-2015.)
⊢ A ∈ V    ⇒   ⊢ ℘1℘A ≈ ℘℘1A
Theorem	enprmaplem1 6077*	Lemma for enprmap 6083. Set up stratification. (Contributed by SF, 3-Mar-2015.)
⊢ W = (r ∈ (A ↑m B) ↦ (◡r “ {x}))    ⇒   ⊢ W ∈ V
Theorem	enprmaplem2 6078*	Lemma for enprmap 6083. Establish functionhood. (Contributed by SF, 3-Mar-2015.)
⊢ W = (r ∈ (A ↑m B) ↦ (◡r “ {x}))    ⇒   ⊢ W Fn (A ↑m B)
Theorem	enprmaplem3 6079*	Lemma for enprmap 6083. The converse of W is a function. (Contributed by SF, 3-Mar-2015.)
⊢ W = (r ∈ (A ↑m B) ↦ (◡r “ {x}))    ⇒   ⊢ ((x ≠ y ∧ A = {x, y}) → Fun ◡W)
Theorem	enprmaplem4 6080*	Lemma for enprmap 6083. More stratification condition setup. (Contributed by SF, 3-Mar-2015.)
⊢ R = (u ∈ B ↦ if(u ∈ p, x, y))    &   ⊢ B ∈ V    ⇒   ⊢ R ∈ V
Theorem	enprmaplem5 6081*	Lemma for enprmap 6083. Establish that ℘B is a subset of the range of W. (Contributed by SF, 3-Mar-2015.)
⊢ W = (r ∈ (A ↑m B) ↦ (◡r “ {x}))    &   ⊢ R = (u ∈ B ↦ if(u ∈ p, x, y))    &   ⊢ B ∈ V    ⇒   ⊢ ((x ≠ y ∧ A = {x, y}) → ℘B ⊆ ran W)
Theorem	enprmaplem6 6082*	Lemma for enprmap 6083. The range of W is ℘B. (Contributed by SF, 3-Mar-2015.)
⊢ W = (r ∈ (A ↑m B) ↦ (◡r “ {x}))    &   ⊢ B ∈ V    ⇒   ⊢ ((x ≠ y ∧ A = {x, y}) → ran W = ℘B)
Theorem	enprmap 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.)
⊢ B ∈ V    ⇒   ⊢ ((x ≠ y ∧ A = {x, y}) → (A ↑m B) ≈ ℘B)
Theorem	enprmapc 6084	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 ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    ⇒   ⊢ ((A ≠ B ∧ P = {A, B}) → (P ↑m C) ≈ ℘C)
Theorem	nenpw1pwlem1 6085*	Lemma for nenpw1pw 6087. Set up stratification. (Contributed by SF, 10-Mar-2015.)
⊢ S = {x ∈ A ∣ ¬ x ∈ (r ‘{x})}    ⇒   ⊢ (A ∈ V → S ∈ V)
Theorem	nenpw1pwlem2 6086*	Lemma for nenpw1pw 6087. Establish the main theorem with an extra hypothesis. (Contributed by SF, 10-Mar-2015.)
⊢ S = {x ∈ A ∣ ¬ x ∈ (r ‘{x})}    ⇒   ⊢ ¬ ℘1A ≈ ℘A
Theorem	nenpw1pw 6087	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.)
⊢ ¬ ℘1A ≈ ℘A
Theorem	enpw 6088	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 → ℘A ≈ ℘B)
2.4.5  Cardinal numbers
Syntax	cncs 6089	Extend the definition of a class to include the set of cardinal numbers.
class NC
Syntax	clec 6090	Extend the definition of a class to include cardinal less than or equal.
class ≤c
Syntax	cltc 6091	Extend the definition of a class to include cardinal strict less than.
class <c
Syntax	cnc 6092	Extend the definition of a class to include the cardinality operation.
class Nc A
Syntax	cmuc 6093	Extend the definition of a class to include cardinal multiplication.
class ·c
Syntax	ctc 6094	Extend the definition of a class to include cardinal type raising.
class Tc A
Syntax	c2c 6095	Extend the definition of a class to include cardinal two.
class 2c
Syntax	c3c 6096	Extend the definition of a class to include cardinal three.
class 3c
Syntax	cce 6097	Extend the definition of a class to include cardinal exponentiation.
class ↑c
Syntax	ctcfn 6098	Extend the definition of a class to include the stratified T-raising function.
class TcFn
Definition	df-ncs 6099	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 6100*	Define cardinal less than or equal. Definition from [Rosser] p. 375. (Contributed by Scott Fenton, 24-Feb-2015.)
⊢ ≤c = {⟨a, b⟩ ∣ ∃x ∈ a ∃y ∈ b x ⊆ y}