Type  Label  Description 
Statement 

Theorem  elpmg 6401 
The predicate "is a partial function." (Contributed by Mario
Carneiro,
14Nov2013.)



Theorem  elpm2g 6402 
The predicate "is a partial function." (Contributed by NM,
31Dec2013.)



Theorem  elpm2r 6403 
Sufficient condition for being a partial function. (Contributed by NM,
31Dec2013.)



Theorem  elpmi 6404 
A partial function is a function. (Contributed by Mario Carneiro,
15Sep2015.)



Theorem  pmfun 6405 
A partial function is a function. (Contributed by Mario Carneiro,
30Jan2014.) (Revised by Mario Carneiro, 26Apr2015.)



Theorem  elmapex 6406 
Eliminate antecedent for mapping theorems: domain can be taken to be a
set. (Contributed by Stefan O'Rear, 8Oct2014.)



Theorem  elmapi 6407 
A mapping is a function, forward direction only with superfluous
antecedent removed. (Contributed by Stefan O'Rear, 10Oct2014.)



Theorem  elmapfn 6408 
A mapping is a function with the appropriate domain. (Contributed by AV,
6Apr2019.)



Theorem  elmapfun 6409 
A mapping is always a function. (Contributed by Stefan O'Rear,
9Oct2014.) (Revised by Stefan O'Rear, 5May2015.)



Theorem  elmapssres 6410 
A restricted mapping is a mapping. (Contributed by Stefan O'Rear,
9Oct2014.) (Revised by Mario Carneiro, 5May2015.)



Theorem  fpmg 6411 
A total function is a partial function. (Contributed by Mario Carneiro,
31Dec2013.)



Theorem  pmss12g 6412 
Subset relation for the set of partial functions. (Contributed by Mario
Carneiro, 31Dec2013.)



Theorem  pmresg 6413 
Elementhood of a restricted function in the set of partial functions.
(Contributed by Mario Carneiro, 31Dec2013.)



Theorem  elmap 6414 
Membership relation for set exponentiation. (Contributed by NM,
8Dec2003.)



Theorem  mapval2 6415* 
Alternate expression for the value of set exponentiation. (Contributed
by NM, 3Nov2007.)



Theorem  elpm 6416 
The predicate "is a partial function." (Contributed by NM,
15Nov2007.) (Revised by Mario Carneiro, 14Nov2013.)



Theorem  elpm2 6417 
The predicate "is a partial function." (Contributed by NM,
15Nov2007.) (Revised by Mario Carneiro, 31Dec2013.)



Theorem  fpm 6418 
A total function is a partial function. (Contributed by NM,
15Nov2007.) (Revised by Mario Carneiro, 31Dec2013.)



Theorem  mapsspm 6419 
Set exponentiation is a subset of partial maps. (Contributed by NM,
15Nov2007.) (Revised by Mario Carneiro, 27Feb2016.)



Theorem  pmsspw 6420 
Partial maps are a subset of the power set of the Cartesian product of
its arguments. (Contributed by Mario Carneiro, 2Jan2017.)



Theorem  mapsspw 6421 
Set exponentiation is a subset of the power set of the Cartesian product
of its arguments. (Contributed by NM, 8Dec2006.) (Revised by Mario
Carneiro, 26Apr2015.)



Theorem  fvmptmap 6422* 
Special case of fvmpt 5365 for operator theorems. (Contributed by NM,
27Nov2007.)



Theorem  map0e 6423 
Set exponentiation with an empty exponent (ordinal number 0) is ordinal
number 1. Exercise 4.42(a) of [Mendelson] p. 255. (Contributed by NM,
10Dec2003.) (Revised by Mario Carneiro, 30Apr2015.)



Theorem  map0b 6424 
Set exponentiation with an empty base is the empty set, provided the
exponent is nonempty. Theorem 96 of [Suppes] p. 89. (Contributed by
NM, 10Dec2003.) (Revised by Mario Carneiro, 26Apr2015.)



Theorem  map0g 6425 
Set exponentiation is empty iff the base is empty and the exponent is
not empty. Theorem 97 of [Suppes] p. 89.
(Contributed by Mario
Carneiro, 30Apr2015.)



Theorem  map0 6426 
Set exponentiation is empty iff the base is empty and the exponent is
not empty. Theorem 97 of [Suppes] p. 89.
(Contributed by NM,
10Dec2003.)



Theorem  mapsn 6427* 
The value of set exponentiation with a singleton exponent. Theorem 98
of [Suppes] p. 89. (Contributed by NM,
10Dec2003.)



Theorem  mapss 6428 
Subset inheritance for set exponentiation. Theorem 99 of [Suppes]
p. 89. (Contributed by NM, 10Dec2003.) (Revised by Mario Carneiro,
26Apr2015.)



Theorem  fdiagfn 6429* 
Functionality of the diagonal map. (Contributed by Stefan O'Rear,
24Jan2015.)



Theorem  fvdiagfn 6430* 
Functionality of the diagonal map. (Contributed by Stefan O'Rear,
24Jan2015.)



Theorem  mapsnconst 6431 
Every singleton map is a constant function. (Contributed by Stefan
O'Rear, 25Mar2015.)



Theorem  mapsncnv 6432* 
Expression for the inverse of the canonical map between a set and its
set of singleton functions. (Contributed by Stefan O'Rear,
21Mar2015.)



Theorem  mapsnf1o2 6433* 
Explicit bijection between a set and its singleton functions.
(Contributed by Stefan O'Rear, 21Mar2015.)



Theorem  mapsnf1o3 6434* 
Explicit bijection in the reverse of mapsnf1o2 6433. (Contributed by
Stefan O'Rear, 24Mar2015.)



2.6.26 Equinumerosity


Syntax  cen 6435 
Extend class definition to include the equinumerosity relation
("approximately equals" symbol)



Syntax  cdom 6436 
Extend class definition to include the dominance relation (curly
lessthanorequal)



Syntax  cfn 6437 
Extend class definition to include the class of all finite sets.



Definition  dfen 6438* 
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 6444. (Contributed by NM, 28Mar1998.)



Definition  dfdom 6439* 
Define the dominance relation. Compare Definition of [Enderton] p. 145.
Typical textbook definitions are derived as brdom 6447 and domen 6448.
(Contributed by NM, 28Mar1998.)



Definition  dffin 6440* 
Define the (proper) class of all finite sets. Similar to Definition
10.29 of [TakeutiZaring] p. 91,
whose "Fin(a)" corresponds to
our " ". This definition is
meaningful whether or not we
accept the Axiom of Infinity axinf2 11528. (Contributed by NM,
22Aug2008.)



Theorem  relen 6441 
Equinumerosity is a relation. (Contributed by NM, 28Mar1998.)



Theorem  reldom 6442 
Dominance is a relation. (Contributed by NM, 28Mar1998.)



Theorem  encv 6443 
If two classes are equinumerous, both classes are sets. (Contributed by
AV, 21Mar2019.)



Theorem  bren 6444* 
Equinumerosity relation. (Contributed by NM, 15Jun1998.)



Theorem  brdomg 6445* 
Dominance relation. (Contributed by NM, 15Jun1998.)



Theorem  brdomi 6446* 
Dominance relation. (Contributed by Mario Carneiro, 26Apr2015.)



Theorem  brdom 6447* 
Dominance relation. (Contributed by NM, 15Jun1998.)



Theorem  domen 6448* 
Dominance in terms of equinumerosity. Example 1 of [Enderton] p. 146.
(Contributed by NM, 15Jun1998.)



Theorem  domeng 6449* 
Dominance in terms of equinumerosity, with the sethood requirement
expressed as an antecedent. Example 1 of [Enderton] p. 146.
(Contributed by NM, 24Apr2004.)



Theorem  ctex 6450 
A countable set is a set. (Contributed by Thierry Arnoux,
29Dec2016.)



Theorem  f1oen3g 6451 
The domain and range of a onetoone, onto function are equinumerous.
This variation of f1oeng 6454 does not require the Axiom of Replacement.
(Contributed by NM, 13Jan2007.) (Revised by Mario Carneiro,
10Sep2015.)



Theorem  f1oen2g 6452 
The domain and range of a onetoone, onto function are equinumerous.
This variation of f1oeng 6454 does not require the Axiom of Replacement.
(Contributed by Mario Carneiro, 10Sep2015.)



Theorem  f1dom2g 6453 
The domain of a onetoone function is dominated by its codomain. This
variation of f1domg 6455 does not require the Axiom of Replacement.
(Contributed by Mario Carneiro, 24Jun2015.)



Theorem  f1oeng 6454 
The domain and range of a onetoone, onto function are equinumerous.
(Contributed by NM, 19Jun1998.)



Theorem  f1domg 6455 
The domain of a onetoone function is dominated by its codomain.
(Contributed by NM, 4Sep2004.)



Theorem  f1oen 6456 
The domain and range of a onetoone, onto function are equinumerous.
(Contributed by NM, 19Jun1998.)



Theorem  f1dom 6457 
The domain of a onetoone function is dominated by its codomain.
(Contributed by NM, 19Jun1998.)



Theorem  isfi 6458* 
Express " is
finite." Definition 10.29 of [TakeutiZaring] p. 91
(whose " " is a predicate instead of a class). (Contributed by
NM, 22Aug2008.)



Theorem  enssdom 6459 
Equinumerosity implies dominance. (Contributed by NM, 31Mar1998.)



Theorem  endom 6460 
Equinumerosity implies dominance. Theorem 15 of [Suppes] p. 94.
(Contributed by NM, 28May1998.)



Theorem  enrefg 6461 
Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed
by NM, 18Jun1998.) (Revised by Mario Carneiro, 26Apr2015.)



Theorem  enref 6462 
Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed
by NM, 25Sep2004.)



Theorem  eqeng 6463 
Equality implies equinumerosity. (Contributed by NM, 26Oct2003.)



Theorem  domrefg 6464 
Dominance is reflexive. (Contributed by NM, 18Jun1998.)



Theorem  en2d 6465* 
Equinumerosity inference from an implicit onetoone onto function.
(Contributed by NM, 27Jul2004.) (Revised by Mario Carneiro,
12May2014.)



Theorem  en3d 6466* 
Equinumerosity inference from an implicit onetoone onto function.
(Contributed by NM, 27Jul2004.) (Revised by Mario Carneiro,
12May2014.)



Theorem  en2i 6467* 
Equinumerosity inference from an implicit onetoone onto function.
(Contributed by NM, 4Jan2004.)



Theorem  en3i 6468* 
Equinumerosity inference from an implicit onetoone onto function.
(Contributed by NM, 19Jul2004.)



Theorem  dom2lem 6469* 
A mapping (first hypothesis) that is onetoone (second hypothesis)
implies its domain is dominated by its codomain. (Contributed by NM,
24Jul2004.)



Theorem  dom2d 6470* 
A mapping (first hypothesis) that is onetoone (second hypothesis)
implies its domain is dominated by its codomain. (Contributed by NM,
24Jul2004.) (Revised by Mario Carneiro, 20May2013.)



Theorem  dom3d 6471* 
A mapping (first hypothesis) that is onetoone (second hypothesis)
implies its domain is dominated by its codomain. (Contributed by Mario
Carneiro, 20May2013.)



Theorem  dom2 6472* 
A mapping (first hypothesis) that is onetoone (second hypothesis)
implies its domain is dominated by its codomain. and can be
read and , as can be inferred from their
distinct variable conditions. (Contributed by NM, 26Oct2003.)



Theorem  dom3 6473* 
A mapping (first hypothesis) that is onetoone (second hypothesis)
implies its domain is dominated by its codomain. and can be
read and , as can be inferred from their
distinct variable conditions. (Contributed by Mario Carneiro,
20May2013.)



Theorem  idssen 6474 
Equality implies equinumerosity. (Contributed by NM, 30Apr1998.)
(Revised by Mario Carneiro, 15Nov2014.)



Theorem  ssdomg 6475 
A set dominates its subsets. Theorem 16 of [Suppes] p. 94. (Contributed
by NM, 19Jun1998.) (Revised by Mario Carneiro, 24Jun2015.)



Theorem  ener 6476 
Equinumerosity is an equivalence relation. (Contributed by NM,
19Mar1998.) (Revised by Mario Carneiro, 15Nov2014.)



Theorem  ensymb 6477 
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by
Mario Carneiro, 26Apr2015.)



Theorem  ensym 6478 
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by
NM, 26Oct2003.) (Revised by Mario Carneiro, 26Apr2015.)



Theorem  ensymi 6479 
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed
by NM, 25Sep2004.)



Theorem  ensymd 6480 
Symmetry of equinumerosity. Deduction form of ensym 6478. (Contributed
by David Moews, 1May2017.)



Theorem  entr 6481 
Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92.
(Contributed by NM, 9Jun1998.)



Theorem  domtr 6482 
Transitivity of dominance relation. Theorem 17 of [Suppes] p. 94.
(Contributed by NM, 4Jun1998.) (Revised by Mario Carneiro,
15Nov2014.)



Theorem  entri 6483 
A chained equinumerosity inference. (Contributed by NM,
25Sep2004.)



Theorem  entr2i 6484 
A chained equinumerosity inference. (Contributed by NM,
25Sep2004.)



Theorem  entr3i 6485 
A chained equinumerosity inference. (Contributed by NM,
25Sep2004.)



Theorem  entr4i 6486 
A chained equinumerosity inference. (Contributed by NM,
25Sep2004.)



Theorem  endomtr 6487 
Transitivity of equinumerosity and dominance. (Contributed by NM,
7Jun1998.)



Theorem  domentr 6488 
Transitivity of dominance and equinumerosity. (Contributed by NM,
7Jun1998.)



Theorem  f1imaeng 6489 
A onetoone function's image under a subset of its domain is equinumerous
to the subset. (Contributed by Mario Carneiro, 15May2015.)



Theorem  f1imaen2g 6490 
A onetoone function's image under a subset of its domain is equinumerous
to the subset. (This version of f1imaen 6491 does not need axsetind 4343.)
(Contributed by Mario Carneiro, 16Nov2014.) (Revised by Mario Carneiro,
25Jun2015.)



Theorem  f1imaen 6491 
A onetoone function's image under a subset of its domain is
equinumerous to the subset. (Contributed by NM, 30Sep2004.)



Theorem  en0 6492 
The empty set is equinumerous only to itself. Exercise 1 of
[TakeutiZaring] p. 88.
(Contributed by NM, 27May1998.)



Theorem  ensn1 6493 
A singleton is equinumerous to ordinal one. (Contributed by NM,
4Nov2002.)



Theorem  ensn1g 6494 
A singleton is equinumerous to ordinal one. (Contributed by NM,
23Apr2004.)



Theorem  enpr1g 6495 
has only
one element. (Contributed by FL, 15Feb2010.)



Theorem  en1 6496* 
A set is equinumerous to ordinal one iff it is a singleton.
(Contributed by NM, 25Jul2004.)



Theorem  en1bg 6497 
A set is equinumerous to ordinal one iff it is a singleton.
(Contributed by Jim Kingdon, 13Apr2020.)



Theorem  reuen1 6498* 
Two ways to express "exactly one". (Contributed by Stefan O'Rear,
28Oct2014.)



Theorem  euen1 6499 
Two ways to express "exactly one". (Contributed by Stefan O'Rear,
28Oct2014.)



Theorem  euen1b 6500* 
Two ways to express " has a unique element". (Contributed by
Mario Carneiro, 9Apr2015.)

