Theorem List for Intuitionistic Logic Explorer - 6601-6700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Definition | df-ixp 6601* |
Definition of infinite Cartesian product of [Enderton] p. 54. Enderton
uses a bold "X" with
written underneath or
as a subscript, as
does Stoll p. 47. Some books use a capital pi, but we will reserve that
notation for products of numbers. Usually represents a class
expression containing free and thus can be thought of as
![B B](_cb.gif) ![( (](lp.gif) ![x x](_x.gif) . Normally,
is not free in ,
although this is
not a requirement of the definition. (Contributed by NM,
28-Sep-2006.)
|
![X_ X_](_bigtimes.gif)
![{ {](lbrace.gif) ![( (](lp.gif) ![{ {](lbrace.gif)
![A A](_ca.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif)
![B B](_cb.gif) ![) )](rp.gif) ![} }](rbrace.gif) |
|
Theorem | dfixp 6602* |
Eliminate the expression ![{ {](lbrace.gif) ![A A](_ca.gif) in df-ixp 6601, under the
assumption that and are
disjoint. This way, we can say that
is bound in
![X_ X_](_bigtimes.gif) ![A A](_ca.gif) even if it
appears free in .
(Contributed by Mario Carneiro, 12-Aug-2016.)
|
![X_ X_](_bigtimes.gif)
![{ {](lbrace.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif)
![B B](_cb.gif) ![) )](rp.gif) ![} }](rbrace.gif) |
|
Theorem | ixpsnval 6603* |
The value of an infinite Cartesian product with a singleton.
(Contributed by AV, 3-Dec-2018.)
|
![( (](lp.gif) ![X_
X_](_bigtimes.gif) ![{ {](lbrace.gif) ![X X](_cx.gif) ![} }](rbrace.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![X X](_cx.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![X X](_cx.gif)
![[_ [_](_ulbrack.gif) ![x x](_x.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![)
)](rp.gif) |
|
Theorem | elixp2 6604* |
Membership in an infinite Cartesian product. See df-ixp 6601 for
discussion of the notation. (Contributed by NM, 28-Sep-2006.)
|
![( (](lp.gif) ![X_ X_](_bigtimes.gif)
![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fvixp 6605* |
Projection of a factor of an indexed Cartesian product. (Contributed by
Mario Carneiro, 11-Jun-2016.)
|
![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![X_ X_](_bigtimes.gif) ![A A](_ca.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![C C](_cc.gif)
![D D](_cd.gif) ![) )](rp.gif) |
|
Theorem | ixpfn 6606* |
A nuple is a function. (Contributed by FL, 6-Jun-2011.) (Revised by
Mario Carneiro, 31-May-2014.)
|
![( (](lp.gif) ![X_ X_](_bigtimes.gif)
![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | elixp 6607* |
Membership in an infinite Cartesian product. (Contributed by NM,
28-Sep-2006.)
|
![( (](lp.gif) ![X_ X_](_bigtimes.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elixpconst 6608* |
Membership in an infinite Cartesian product of a constant .
(Contributed by NM, 12-Apr-2008.)
|
![( (](lp.gif) ![X_ X_](_bigtimes.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | ixpconstg 6609* |
Infinite Cartesian product of a constant . (Contributed by Mario
Carneiro, 11-Jan-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![X_ X_](_bigtimes.gif)
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ixpconst 6610* |
Infinite Cartesian product of a constant . (Contributed by NM,
28-Sep-2006.)
|
![X_ X_](_bigtimes.gif)
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | ixpeq1 6611* |
Equality theorem for infinite Cartesian product. (Contributed by NM,
29-Sep-2006.)
|
![( (](lp.gif) ![X_
X_](_bigtimes.gif)
![X_ X_](_bigtimes.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | ixpeq1d 6612* |
Equality theorem for infinite Cartesian product. (Contributed by Mario
Carneiro, 11-Jun-2016.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![X_ X_](_bigtimes.gif) ![X_ X_](_bigtimes.gif)
![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | ss2ixp 6613 |
Subclass theorem for infinite Cartesian product. (Contributed by NM,
29-Sep-2006.) (Revised by Mario Carneiro, 12-Aug-2016.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![X_
X_](_bigtimes.gif) ![X_ X_](_bigtimes.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | ixpeq2 6614 |
Equality theorem for infinite Cartesian product. (Contributed by NM,
29-Sep-2006.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![X_
X_](_bigtimes.gif)
![X_ X_](_bigtimes.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | ixpeq2dva 6615* |
Equality theorem for infinite Cartesian product. (Contributed by Mario
Carneiro, 11-Jun-2016.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![( (](lp.gif) ![X_ X_](_bigtimes.gif) ![X_ X_](_bigtimes.gif)
![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | ixpeq2dv 6616* |
Equality theorem for infinite Cartesian product. (Contributed by Mario
Carneiro, 11-Jun-2016.)
|
![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![X_ X_](_bigtimes.gif) ![X_ X_](_bigtimes.gif)
![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | cbvixp 6617* |
Change bound variable in an indexed Cartesian product. (Contributed by
Jeff Madsen, 20-Jun-2011.)
|
![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![( (](lp.gif)
![C C](_cc.gif) ![X_ X_](_bigtimes.gif)
![X_ X_](_bigtimes.gif) ![C C](_cc.gif) |
|
Theorem | cbvixpv 6618* |
Change bound variable in an indexed Cartesian product. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
![( (](lp.gif) ![C C](_cc.gif) ![X_ X_](_bigtimes.gif) ![X_ X_](_bigtimes.gif) ![C C](_cc.gif) |
|
Theorem | nfixpxy 6619* |
Bound-variable hypothesis builder for indexed Cartesian product.
(Contributed by Mario Carneiro, 15-Oct-2016.) (Revised by Jim Kingdon,
15-Feb-2023.)
|
![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![X_ X_](_bigtimes.gif) ![B B](_cb.gif) |
|
Theorem | nfixp1 6620 |
The index variable in an indexed Cartesian product is not free.
(Contributed by Jeff Madsen, 19-Jun-2011.) (Revised by Mario Carneiro,
15-Oct-2016.)
|
![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![X_ X_](_bigtimes.gif) ![B B](_cb.gif) |
|
Theorem | ixpprc 6621* |
A cartesian product of proper-class many sets is empty, because any
function in the cartesian product has to be a set with domain ,
which is not possible for a proper class domain. (Contributed by Mario
Carneiro, 25-Jan-2015.)
|
![( (](lp.gif) ![X_ X_](_bigtimes.gif)
![(/) (/)](varnothing.gif) ![) )](rp.gif) |
|
Theorem | ixpf 6622* |
A member of an infinite Cartesian product maps to the indexed union of
the product argument. Remark in [Enderton] p. 54. (Contributed by NM,
28-Sep-2006.)
|
![( (](lp.gif) ![X_ X_](_bigtimes.gif)
![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![U_ U_](_cupbar.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | uniixp 6623* |
The union of an infinite Cartesian product is included in a Cartesian
product. (Contributed by NM, 28-Sep-2006.) (Revised by Mario Carneiro,
24-Jun-2015.)
|
![U.
U.](bigcup.gif) ![X_ X_](_bigtimes.gif) ![( (](lp.gif) ![U_ U_](_cupbar.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | ixpexgg 6624* |
The existence of an infinite Cartesian product. is normally a
free-variable parameter in . Remark in Enderton p. 54.
(Contributed by NM, 28-Sep-2006.) (Revised by Jim Kingdon,
15-Feb-2023.)
|
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![V V](_cv.gif) ![X_ X_](_bigtimes.gif)
![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | ixpin 6625* |
The intersection of two infinite Cartesian products. (Contributed by
Mario Carneiro, 3-Feb-2015.)
|
![X_ X_](_bigtimes.gif)
![( (](lp.gif)
![C C](_cc.gif) ![( (](lp.gif) ![X_ X_](_bigtimes.gif) ![X_ X_](_bigtimes.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | ixpiinm 6626* |
The indexed intersection of a collection of infinite Cartesian products.
(Contributed by Mario Carneiro, 6-Feb-2015.) (Revised by Jim Kingdon,
15-Feb-2023.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![X_ X_](_bigtimes.gif) ![|^|_ |^|_](_capbar.gif)
![|^|_ |^|_](_capbar.gif) ![X_ X_](_bigtimes.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | ixpintm 6627* |
The intersection of a collection of infinite Cartesian products.
(Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Jim Kingdon,
15-Feb-2023.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![X_ X_](_bigtimes.gif) ![|^| |^|](bigcap.gif) ![|^|_ |^|_](_capbar.gif) ![X_ X_](_bigtimes.gif) ![y y](_y.gif) ![) )](rp.gif) |
|
Theorem | ixp0x 6628 |
An infinite Cartesian product with an empty index set. (Contributed by
NM, 21-Sep-2007.)
|
![X_ X_](_bigtimes.gif)
![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![} }](rbrace.gif) |
|
Theorem | ixpssmap2g 6629* |
An infinite Cartesian product is a subset of set exponentiation. This
version of ixpssmapg 6630 avoids ax-coll 4051. (Contributed by Mario
Carneiro, 16-Nov-2014.)
|
![( (](lp.gif) ![U_ U_](_cupbar.gif) ![X_
X_](_bigtimes.gif) ![( (](lp.gif) ![U_ U_](_cupbar.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ixpssmapg 6630* |
An infinite Cartesian product is a subset of set exponentiation.
(Contributed by Jeff Madsen, 19-Jun-2011.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![X_
X_](_bigtimes.gif) ![( (](lp.gif) ![U_ U_](_cupbar.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | 0elixp 6631 |
Membership of the empty set in an infinite Cartesian product.
(Contributed by Steve Rodriguez, 29-Sep-2006.)
|
![X_ X_](_bigtimes.gif) ![A A](_ca.gif) |
|
Theorem | ixpm 6632* |
If an infinite Cartesian product of a family ![B B](_cb.gif) ![( (](lp.gif) ![x x](_x.gif) is inhabited,
every ![B B](_cb.gif) ![( (](lp.gif) ![x x](_x.gif) is inhabited. (Contributed by Mario Carneiro,
22-Jun-2016.) (Revised by Jim Kingdon, 16-Feb-2023.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![X_ X_](_bigtimes.gif) ![A. A.](forall.gif) ![E. E.](exists.gif)
![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | ixp0 6633 |
The infinite Cartesian product of a family ![B B](_cb.gif) ![( (](lp.gif) ![x x](_x.gif) with an empty
member is empty. (Contributed by NM, 1-Oct-2006.) (Revised by Jim
Kingdon, 16-Feb-2023.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![X_ X_](_bigtimes.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) |
|
Theorem | ixpssmap 6634* |
An infinite Cartesian product is a subset of set exponentiation. Remark
in [Enderton] p. 54. (Contributed by
NM, 28-Sep-2006.)
|
![X_ X_](_bigtimes.gif) ![( (](lp.gif) ![U_ U_](_cupbar.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | resixp 6635* |
Restriction of an element of an infinite Cartesian product.
(Contributed by FL, 7-Nov-2011.) (Proof shortened by Mario Carneiro,
31-May-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![X_ X_](_bigtimes.gif)
![C C](_cc.gif) ![( (](lp.gif) ![B B](_cb.gif) ![X_ X_](_bigtimes.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | mptelixpg 6636* |
Condition for an explicit member of an indexed product. (Contributed by
Stefan O'Rear, 4-Jan-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![J J](_cj.gif) ![X_ X_](_bigtimes.gif)
![A.
A.](forall.gif)
![K K](_ck.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | elixpsn 6637* |
Membership in a class of singleton functions. (Contributed by Stefan
O'Rear, 24-Jan-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![X_ X_](_bigtimes.gif)
![{ {](lbrace.gif) ![A A](_ca.gif) ![} }](rbrace.gif)
![E. E.](exists.gif)
![{ {](lbrace.gif) ![<. <.](langle.gif) ![A A](_ca.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ixpsnf1o 6638* |
A bijection between a class and single-point functions to it.
(Contributed by Stefan O'Rear, 24-Jan-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![I I](_ci.gif)
![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![( (](lp.gif)
![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto->
-1-1-onto->](onetooneonto.gif) ![X_ X_](_bigtimes.gif) ![{ {](lbrace.gif) ![I I](_ci.gif) ![} }](rbrace.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | mapsnf1o 6639* |
A bijection between a set and single-point functions to it.
(Contributed by Stefan O'Rear, 24-Jan-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![I I](_ci.gif)
![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![I I](_ci.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
2.6.27 Equinumerosity
|
|
Syntax | cen 6640 |
Extend class definition to include the equinumerosity relation
("approximately equals" symbol)
|
![~~ ~~](approx.gif) |
|
Syntax | cdom 6641 |
Extend class definition to include the dominance relation (curly
less-than-or-equal)
|
![~<_ ~<_](preccurlyeq.gif) |
|
Syntax | cfn 6642 |
Extend class definition to include the class of all finite sets.
|
![Fin Fin](_fin.gif) |
|
Definition | df-en 6643* |
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 6649. (Contributed by NM, 28-Mar-1998.)
|
![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![: :](colon.gif) ![x x](_x.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![y y](_y.gif) ![} }](rbrace.gif) |
|
Definition | df-dom 6644* |
Define the dominance relation. Compare Definition of [Enderton] p. 145.
Typical textbook definitions are derived as brdom 6652 and domen 6653.
(Contributed by NM, 28-Mar-1998.)
|
![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![: :](colon.gif) ![x x](_x.gif) ![-1-1-> -1-1->](onetoone.gif) ![y y](_y.gif) ![} }](rbrace.gif) |
|
Definition | df-fin 6645* |
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 ax-inf2 13345. (Contributed by NM,
22-Aug-2008.)
|
![{ {](lbrace.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![} }](rbrace.gif) |
|
Theorem | relen 6646 |
Equinumerosity is a relation. (Contributed by NM, 28-Mar-1998.)
|
![~~ ~~](approx.gif) |
|
Theorem | reldom 6647 |
Dominance is a relation. (Contributed by NM, 28-Mar-1998.)
|
![~<_ ~<_](preccurlyeq.gif) |
|
Theorem | encv 6648 |
If two classes are equinumerous, both classes are sets. (Contributed by
AV, 21-Mar-2019.)
|
![( (](lp.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | bren 6649* |
Equinumerosity relation. (Contributed by NM, 15-Jun-1998.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | brdomg 6650* |
Dominance relation. (Contributed by NM, 15-Jun-1998.)
|
![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | brdomi 6651* |
Dominance relation. (Contributed by Mario Carneiro, 26-Apr-2015.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | brdom 6652* |
Dominance relation. (Contributed by NM, 15-Jun-1998.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | domen 6653* |
Dominance in terms of equinumerosity. Example 1 of [Enderton] p. 146.
(Contributed by NM, 15-Jun-1998.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | domeng 6654* |
Dominance in terms of equinumerosity, with the sethood requirement
expressed as an antecedent. Example 1 of [Enderton] p. 146.
(Contributed by NM, 24-Apr-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ctex 6655 |
A class dominated by is a set. See also ctfoex 7011 which says that
a countable class is a set. (Contributed by Thierry Arnoux, 29-Dec-2016.)
(Proof shortened by Jim Kingdon, 13-Mar-2023.)
|
![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | f1oen3g 6656 |
The domain and range of a one-to-one, onto function are equinumerous.
This variation of f1oeng 6659 does not require the Axiom of Replacement.
(Contributed by NM, 13-Jan-2007.) (Revised by Mario Carneiro,
10-Sep-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![B B](_cb.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | f1oen2g 6657 |
The domain and range of a one-to-one, onto function are equinumerous.
This variation of f1oeng 6659 does not require the Axiom of Replacement.
(Contributed by Mario Carneiro, 10-Sep-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![B B](_cb.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | f1dom2g 6658 |
The domain of a one-to-one function is dominated by its codomain. This
variation of f1domg 6660 does not require the Axiom of Replacement.
(Contributed by Mario Carneiro, 24-Jun-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![B B](_cb.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | f1oeng 6659 |
The domain and range of a one-to-one, onto function are equinumerous.
(Contributed by NM, 19-Jun-1998.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![B B](_cb.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | f1domg 6660 |
The domain of a one-to-one function is dominated by its codomain.
(Contributed by NM, 4-Sep-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | f1oen 6661 |
The domain and range of a one-to-one, onto function are equinumerous.
(Contributed by NM, 19-Jun-1998.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto->
-1-1-onto->](onetooneonto.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | f1dom 6662 |
The domain of a one-to-one function is dominated by its codomain.
(Contributed by NM, 19-Jun-1998.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif)
![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | isfi 6663* |
Express " is
finite." Definition 10.29 of [TakeutiZaring] p. 91
(whose " " is a predicate instead of a class). (Contributed by
NM, 22-Aug-2008.)
|
![( (](lp.gif) ![E. E.](exists.gif)
![x x](_x.gif) ![) )](rp.gif) |
|
Theorem | enssdom 6664 |
Equinumerosity implies dominance. (Contributed by NM, 31-Mar-1998.)
|
![~<_ ~<_](preccurlyeq.gif) |
|
Theorem | endom 6665 |
Equinumerosity implies dominance. Theorem 15 of [Suppes] p. 94.
(Contributed by NM, 28-May-1998.)
|
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | enrefg 6666 |
Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed
by NM, 18-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | enref 6667 |
Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed
by NM, 25-Sep-2004.)
|
![A A](_ca.gif) |
|
Theorem | eqeng 6668 |
Equality implies equinumerosity. (Contributed by NM, 26-Oct-2003.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | domrefg 6669 |
Dominance is reflexive. (Contributed by NM, 18-Jun-1998.)
|
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | en2d 6670* |
Equinumerosity inference from an implicit one-to-one onto function.
(Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro,
12-May-2014.)
|
![( (](lp.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![( (](lp.gif)
![_V _V](rmcv.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![( (](lp.gif)
![D D](_cd.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | en3d 6671* |
Equinumerosity inference from an implicit one-to-one onto function.
(Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro,
12-May-2014.)
|
![( (](lp.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | en2i 6672* |
Equinumerosity inference from an implicit one-to-one onto function.
(Contributed by NM, 4-Jan-2004.)
|
![( (](lp.gif)
![_V _V](rmcv.gif) ![( (](lp.gif)
![_V _V](rmcv.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![B B](_cb.gif) |
|
Theorem | en3i 6673* |
Equinumerosity inference from an implicit one-to-one onto function.
(Contributed by NM, 19-Jul-2004.)
|
![( (](lp.gif)
![B B](_cb.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![B B](_cb.gif) |
|
Theorem | dom2lem 6674* |
A mapping (first hypothesis) that is one-to-one (second hypothesis)
implies its domain is dominated by its codomain. (Contributed by NM,
24-Jul-2004.)
|
![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | dom2d 6675* |
A mapping (first hypothesis) that is one-to-one (second hypothesis)
implies its domain is dominated by its codomain. (Contributed by NM,
24-Jul-2004.) (Revised by Mario Carneiro, 20-May-2013.)
|
![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | dom3d 6676* |
A mapping (first hypothesis) that is one-to-one (second hypothesis)
implies its domain is dominated by its codomain. (Contributed by Mario
Carneiro, 20-May-2013.)
|
![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | dom2 6677* |
A mapping (first hypothesis) that is one-to-one (second hypothesis)
implies its domain is dominated by its codomain. and can be
read ![C C](_cc.gif) ![( (](lp.gif) ![x x](_x.gif) and ![D D](_cd.gif) ![( (](lp.gif) ![y y](_y.gif) , as can be inferred from their
distinct variable conditions. (Contributed by NM, 26-Oct-2003.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif)
![y y](_y.gif) ![)
)](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | dom3 6678* |
A mapping (first hypothesis) that is one-to-one (second hypothesis)
implies its domain is dominated by its codomain. and can be
read ![C C](_cc.gif) ![( (](lp.gif) ![x x](_x.gif) and ![D D](_cd.gif) ![( (](lp.gif) ![y y](_y.gif) , as can be inferred from their
distinct variable conditions. (Contributed by Mario Carneiro,
20-May-2013.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif)
![y y](_y.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | idssen 6679 |
Equality implies equinumerosity. (Contributed by NM, 30-Apr-1998.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
![~~ ~~](approx.gif) |
|
Theorem | ssdomg 6680 |
A set dominates its subsets. Theorem 16 of [Suppes] p. 94. (Contributed
by NM, 19-Jun-1998.) (Revised by Mario Carneiro, 24-Jun-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ener 6681 |
Equinumerosity is an equivalence relation. (Contributed by NM,
19-Mar-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
![_V _V](rmcv.gif) |
|
Theorem | ensymb 6682 |
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by
Mario Carneiro, 26-Apr-2015.)
|
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | ensym 6683 |
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by
NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | ensymi 6684 |
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed
by NM, 25-Sep-2004.)
|
![A A](_ca.gif) |
|
Theorem | ensymd 6685 |
Symmetry of equinumerosity. Deduction form of ensym 6683. (Contributed
by David Moews, 1-May-2017.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | entr 6686 |
Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92.
(Contributed by NM, 9-Jun-1998.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | domtr 6687 |
Transitivity of dominance relation. Theorem 17 of [Suppes] p. 94.
(Contributed by NM, 4-Jun-1998.) (Revised by Mario Carneiro,
15-Nov-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | entri 6688 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
![C C](_cc.gif) |
|
Theorem | entr2i 6689 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
![A A](_ca.gif) |
|
Theorem | entr3i 6690 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
![C C](_cc.gif) |
|
Theorem | entr4i 6691 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
![C C](_cc.gif) |
|
Theorem | endomtr 6692 |
Transitivity of equinumerosity and dominance. (Contributed by NM,
7-Jun-1998.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | domentr 6693 |
Transitivity of dominance and equinumerosity. (Contributed by NM,
7-Jun-1998.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | f1imaeng 6694 |
A one-to-one function's image under a subset of its domain is equinumerous
to the subset. (Contributed by Mario Carneiro, 15-May-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif)
![V V](_cv.gif) ![( (](lp.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![C C](_cc.gif)
![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | f1imaen2g 6695 |
A one-to-one function's image under a subset of its domain is equinumerous
to the subset. (This version of f1imaen 6696 does not need ax-setind 4460.)
(Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro,
25-Jun-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif)
![V V](_cv.gif) ![( (](lp.gif) ![V V](_cv.gif) ![) )](rp.gif)
![( (](lp.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | f1imaen 6696 |
A one-to-one function's image under a subset of its domain is
equinumerous to the subset. (Contributed by NM, 30-Sep-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![A A](_ca.gif) ![( (](lp.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | en0 6697 |
The empty set is equinumerous only to itself. Exercise 1 of
[TakeutiZaring] p. 88.
(Contributed by NM, 27-May-1998.)
|
![( (](lp.gif)
![(/) (/)](varnothing.gif) ![) )](rp.gif) |
|
Theorem | ensn1 6698 |
A singleton is equinumerous to ordinal one. (Contributed by NM,
4-Nov-2002.)
|
![{ {](lbrace.gif) ![A A](_ca.gif) ![1o 1o](_1o.gif) |
|
Theorem | ensn1g 6699 |
A singleton is equinumerous to ordinal one. (Contributed by NM,
23-Apr-2004.)
|
![( (](lp.gif) ![{ {](lbrace.gif) ![A A](_ca.gif) ![1o 1o](_1o.gif) ![) )](rp.gif) |
|
Theorem | enpr1g 6700 |
![{ {](lbrace.gif) ![A A](_ca.gif) ![A A](_ca.gif) has only
one element. (Contributed by FL, 15-Feb-2010.)
|
![( (](lp.gif) ![{ {](lbrace.gif) ![A A](_ca.gif) ![A A](_ca.gif) ![1o 1o](_1o.gif) ![) )](rp.gif) |