 Home New Foundations ExplorerTheorem List (p. 61 of 64) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  NFE Home Page  >  Theorem List Contents       This page: Page List

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

Definitiondf-map 6001* Define the mapping operation or set exponentiation. The set of all functions that map from B to A is written (Am 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 (Am 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})

Definitiondf-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 (Apm 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 V, y V {f (y × x) Fun f})

Theoremmapexi 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 V    &   B V       {f f:A–→B} V

Theoremmapprc 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 V → {f f:A–→B} = )

Theorempmex 6005* 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)

Theoremmapex 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 C B D) → {f f:A–→B} V)

Theoremfnmap 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

Theoremfnpm 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

Theoremmapvalg 6009* The value of set exponentiation. (Am 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) → (Am B) = {f f:B–→A})

Theorempmvalg 6010* The value of the partial mapping operation. (Apm 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) → (Apm B) = {f (B × A) Fun f})

Theoremmapval 6011* The value of set exponentiation (inference version). (Am 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       (Am B) = {f f:B–→A}

Theoremelmapg 6012 Membership relation for set exponentiation. (Contributed by set.mm contributors, 17-Oct-2006.)
((A V B W C X) → (C (Am B) ↔ C:B–→A))

Theoremelpmg 6013 The predicate "is a partial function." (Contributed by set.mm contributors, 14-Nov-2013.)
((A V B W C X) → (C (Apm B) ↔ (Fun C C (B × A))))

Theoremelpm2g 6014 The predicate "is a partial function." (Contributed by set.mm contributors, 31-Dec-2013.)
((A V B W F X) → (F (Apm B) ↔ (F:dom F–→A dom F B)))

Theorempmfun 6015 A partial function is a function. (Contributed by Mario Carneiro, 30-Jan-2014.)
(F (Apm B) → Fun F)

Theoremelmapi 6016 A mapping is a function, forward direction only with antecedents removed. (Contributed by set.mm contributors, 25-Feb-2015.)
(A (Bm C) → A:C–→B)

Theoremelmap 6017 Membership relation for set exponentiation. (Contributed by set.mm contributors, 8-Dec-2003.)
A V    &   B V    &   F V       (F (Am B) ↔ F:B–→A)

Theoremmapval2 6018* Alternate expression for the value of set exponentiation. (Contributed by set.mm contributors, 3-Nov-2007.)
A V    &   B V    &   F V       (Am B) = ((B × A) ∩ {f f Fn B})

Theoremelpm 6019 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 (Apm B) ↔ (Fun F F (B × A)))

Theoremelpm2 6020 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 (Apm B) ↔ (F:dom F–→A dom F B))

Theoremmapsspm 6021 Set exponentiation is a subset of partial maps. (Contributed by set.mm contributors, 15-Nov-2007.)
(Am B) (Apm B)

Theoremmapsspw 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.)
(Am B) (B × A)

Theoremmap0e 6023 Set exponentiation with an empty exponent is the unit class of the empty set. (Contributed by set.mm contributors, 10-Dec-2003.)
A V       (Am ) = {}

Theoremmap0b 6024 Set exponentiation with an empty base is the empty set, provided the exponent is non-empty. 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) = )

Theoremmap0 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 V    &   B V       ((Am B) = ↔ (A = B))

Theoremmapsn 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 V    &   B V       (Am {B}) = {f y A f = {B, y}}

Theoremmapss 6027 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 → (Am C) (Bm C))

2.4.4  Equinumerosity

Syntaxcen 6028 Extend class definition to include the equinumerosity relation ("approximately equals" symbol)
class

Definitiondf-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 f f:x1-1-ontoy}

Theorembren 6030* Equinumerosity relationship. (Contributed by SF, 23-Feb-2015.)
(ABf f:A1-1-ontoB)

Theoremenex 6031 The equinumerosity relationship is a set. (Contributed by SF, 23-Feb-2015.)
V

Theoremf1oeng 6032 The domain and range of a one-to-one, onto function are equinumerous. (Contributed by SF, 23-Feb-2015.)
((F C F:A1-1-ontoB) → AB)

Theoremf1oen 6033 The domain and range of a one-to-one, onto function are equinumerous. (Contributed by SF, 19-Jun-1998.)
F V       (F:A1-1-ontoBAB)

Theoremenrflxg 6034 Equinumerosity is reflexive. (Contributed by SF, 23-Feb-2015.)
(A VAA)

Theoremenrflx 6035 Equinumerosity is reflexive. (Contributed by SF, 23-Feb-2015.)
A V       AA

Theoremensymi 6036 Equinumerosity is symmetric. (Contributed by SF, 23-Feb-2015.)
(ABBA)

Theoremensym 6037 Equinumerosity is symmetric. (Contributed by SF, 23-Feb-2015.)
(ABBA)

Theorementr 6038 Equinumerosity is transitive. (Contributed by SF, 23-Feb-2015.)
((AB BC) → AC)

Theoremener 6039 Equinumerosity is an equivalence relationship over the universe. (Contributed by SF, 23-Feb-2015.)
Er V

Theoremidssen 6040 Equality implies equinumerosity. (Contributed by SF, 30-Apr-1998.)
I

Theoremdmen 6041 The domain of equinumerosity. (Contributed by SF, 10-May-1998.)
dom ≈ = V

Theoremen0 6042 The empty set is equinumerous only to itself. Exercise 1 of [TakeutiZaring] p. 88. (Contributed by SF, 27-May-1998.)
(AA = )

Theoremfundmen 6043 A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98. (Contributed by SF, 23-Feb-2015.)
F V       (Fun F → dom FF)

Theoremfundmeng 6044 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 FF)

Theoremcnven 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 VAA)

Theoremfndmeng 6046 A function is equinumerate to its domain. (Contributed by Paul Chapman, 22-Jun-2011.)
((F Fn A F C) → AF)

Theoremen2sn 6047 Two singletons are equinumerous. (Contributed by set.mm contributors, 9-Nov-2003.)
((A C B D) → {A} ≈ {B})

Theoremunen 6048 Equinumerosity of union of disjoint sets. Theorem 4 of [Suppes] p. 92. (Contributed by set.mm contributors, 11-Jun-1998.)
(((AB CD) ((AC) = (BD) = )) → (AC) ≈ (BD))

Theoremxpsnen 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 V    &   B V       (A × {B}) ≈ A

Theoremxpsneng 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 V B W) → (A × {B}) ≈ A)

Theoremendisj 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 V    &   B V       xy((xA yB) (xy) = )

Theoremxpcomen 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 V    &   B V       (A × B) ≈ (B × A)

Theoremxpcomeng 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 V B W) → (A × B) ≈ (B × A))

Theoremxpsnen2g 6054 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)

Theoremxpen 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.)
((AB CD) → (A × C) ≈ (B × D))

Theoremxpassenlem 6056 Lemma for xpassen 6057. 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))

Theoremxpassen 6057 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))

Theoremensn 6058 Two singletons are equinumerous. Theorem XI.1.10 of [Rosser] p. 348. (Contributed by SF, 25-Feb-2015.)
A V    &   B V       {A} ≈ {B}

Theoremenadjlem1 6059 Lemma for enadj 6060. 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}))

Theoremenadj 6060 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) → AB)

Theoremenpw1lem1 6061* Lemma for enpw1 6062. Set up stratification for the reverse direction. (Contributed by SF, 26-Feb-2015.)
{x, y {x}g{y}} V

Theoremenpw1 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.)
(AB1A1B)

Theoremenmap2lem1 6063* Lemma for enmap2 6068. Set up stratification. (Contributed by SF, 26-Feb-2015.)
W = (s (Gm A) (s r))       W V

Theoremenmap2lem2 6064* Lemma for enmap2 6068. Establish the functionhood and domain of W. (Contributed by SF, 26-Feb-2015.)
W = (s (Gm a) (s r))       W Fn (Gm a)

Theoremenmap2lem3 6065* Lemma for enmap2 6068. Binary relationship condition over W. (Contributed by SF, 26-Feb-2015.)
W = (s (Gm a) (s r))       (r:a1-1-ontob → (SWTS = (T r)))

Theoremenmap2lem4 6066* Lemma for enmap2 6068. The converse of W is a function. (Contributed by SF, 26-Feb-2015.)
W = (s (Gm a) (s r))       (r:a1-1-ontob → Fun W)

Theoremenmap2lem5 6067* Lemma for enmap2 6068. Calculate the range of W. (Contributed by SF, 26-Feb-2015.)
W = (s (Gm a) (s r))       (r:a1-1-ontob → ran W = (Gm b))

Theoremenmap2 6068 Set exponentiation preserves equinumerosity in the second argument. Theorem XI.1.22 of [Rosser] p. 357. (Contributed by SF, 26-Feb-2015.)
(AB → (Cm A) ≈ (Cm B))

Theoremenmap1lem1 6069* Lemma for enmap1 6074. Set up stratification. (Contributed by SF, 3-Mar-2015.)
W = (s (Am G) (r s))       W V

Theoremenmap1lem2 6070* Lemma for enmap1 6074. Establish functionhood. (Contributed by SF, 3-Mar-2015.)
W = (s (Am G) (r s))       W Fn (Am G)

Theoremenmap1lem3 6071* Lemma for enmap2 6068. Binary relationship condition over W. (Contributed by SF, 3-Mar-2015.)
W = (s (Am G) (r s))       (r:A1-1-ontoB → (SWTS = (r T)))

Theoremenmap1lem4 6072* Lemma for enmap2 6068. The converse of W is a function. (Contributed by SF, 3-Mar-2015.)
W = (s (Am G) (r s))       (r:A1-1-ontoB → Fun W)

Theoremenmap1lem5 6073* Lemma for enmap2 6068. Calculate the range of W. (Contributed by SF, 3-Mar-2015.)
W = (s (Am G) (r s))       (r:A1-1-ontoB → ran W = (Bm G))

Theoremenmap1 6074 Set exponentiation preserves equinumerosity in the first argument. Theorem XI.1.23 of [Rosser] p. 357. (Contributed by SF, 3-Mar-2015.)
(AB → (Am C) ≈ (Bm C))

Theoremenpw1pw 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 V       1A1A

Theoremenprmaplem1 6076* Lemma for enprmap 6082. Set up stratification. (Contributed by SF, 3-Mar-2015.)
W = (r (Am B) (r “ {x}))       W V

Theoremenprmaplem2 6077* Lemma for enprmap 6082. Establish functionhood. (Contributed by SF, 3-Mar-2015.)
W = (r (Am B) (r “ {x}))       W Fn (Am B)

Theoremenprmaplem3 6078* Lemma for enprmap 6082. The converse of W is a function. (Contributed by SF, 3-Mar-2015.)
W = (r (Am B) (r “ {x}))       ((xy A = {x, y}) → Fun W)

Theoremenprmaplem4 6079* Lemma for enprmap 6082. More stratification condition setup. (Contributed by SF, 3-Mar-2015.)
R = (u B if(u p, x, y))    &   B V       R V

Theoremenprmaplem5 6080* Lemma for enprmap 6082. Establish that B is a subset of the range of W. (Contributed by SF, 3-Mar-2015.)
W = (r (Am B) (r “ {x}))    &   R = (u B if(u p, x, y))    &   B V       ((xy A = {x, y}) → B ran W)

Theoremenprmaplem6 6081* Lemma for enprmap 6082. The range of W is B. (Contributed by SF, 3-Mar-2015.)
W = (r (Am B) (r “ {x}))    &   B V       ((xy A = {x, y}) → ran W = B)

Theoremenprmap 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 V       ((xy A = {x, y}) → (Am B) ≈ B)

Theoremenprmapc 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 V    &   B V    &   C V       ((AB P = {A, B}) → (Pm C) ≈ C)

Theoremnenpw1pwlem1 6084* Lemma for nenpw1pw 6086. Set up stratification. (Contributed by SF, 10-Mar-2015.)
S = {x A ¬ x (r ‘{x})}       (A VS V)

Theoremnenpw1pwlem2 6085* Lemma for nenpw1pw 6086. Establish the main theorem with an extra hypothesis. (Contributed by SF, 10-Mar-2015.)
S = {x A ¬ x (r ‘{x})}        ¬ 1AA

Theoremnenpw1pw 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.)
¬ 1AA

Theoremenpw 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.)
(ABAB)

2.4.5  Cardinal numbers

Syntaxcncs 6088 Extend the definition of a class to include the set of cardinal numbers.
class NC

Syntaxclec 6089 Extend the definition of a class to include cardinal less than or equal.
class c

Syntaxcltc 6090 Extend the definition of a class to include cardinal strict less than.
class <c

Syntaxcnc 6091 Extend the definition of a class to include the cardinality operation.
class Nc A

Syntaxcmuc 6092 Extend the definition of a class to include cardinal multiplication.
class ·c

Syntaxctc 6093 Extend the definition of a class to include cardinal type raising.
class Tc A

Syntaxc2c 6094 Extend the definition of a class to include cardinal two.
class 2c

Syntaxc3c 6095 Extend the definition of a class to include cardinal three.
class 3c

Syntaxcce 6096 Extend the definition of a class to include cardinal exponentiation.
class c

Syntaxctcfn 6097 Extend the definition of a class to include the stratified T-raising function.
class TcFn

Definitiondf-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 / ≈ )

Definitiondf-lec 6099* 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}

Definitiondf-ltc 6100 Define cardinal less than. Definition from [Rosser] p. 375. (Contributed by Scott Fenton, 24-Feb-2015.)
<c = ( ≤c I )

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-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6337
 Copyright terms: Public domain < Previous  Next >