Theorem List for Intuitionistic Logic Explorer - 6601-6700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | elpmi 6601 |
A partial function is a function. (Contributed by Mario Carneiro,
15-Sep-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![F F](_cf.gif) ![--> -->](longrightarrow.gif)
![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | pmfun 6602 |
A partial function is a function. (Contributed by Mario Carneiro,
30-Jan-2014.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![F F](_cf.gif) ![) )](rp.gif) |
|
Theorem | elmapex 6603 |
Eliminate antecedent for mapping theorems: domain can be taken to be a
set. (Contributed by Stefan O'Rear, 8-Oct-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif)
![_V _V](rmcv.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | elmapi 6604 |
A mapping is a function, forward direction only with superfluous
antecedent removed. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![A A](_ca.gif) ![: :](colon.gif) ![C C](_cc.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | elmapfn 6605 |
A mapping is a function with the appropriate domain. (Contributed by AV,
6-Apr-2019.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | elmapfun 6606 |
A mapping is always a function. (Contributed by Stefan O'Rear,
9-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | elmapssres 6607 |
A restricted mapping is a mapping. (Contributed by Stefan O'Rear,
9-Oct-2014.) (Revised by Mario Carneiro, 5-May-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![C C](_cc.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fpmg 6608 |
A total function is a partial function. (Contributed by Mario Carneiro,
31-Dec-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | pmss12g 6609 |
Subset relation for the set of partial functions. (Contributed by Mario
Carneiro, 31-Dec-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif)
![W W](_cw.gif) ![) )](rp.gif)
![( (](lp.gif) ![B
B](_cb.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | pmresg 6610 |
Elementhood of a restricted function in the set of partial functions.
(Contributed by Mario Carneiro, 31-Dec-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elmap 6611 |
Membership relation for set exponentiation. (Contributed by NM,
8-Dec-2003.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![F F](_cf.gif) ![: :](colon.gif) ![B B](_cb.gif) ![--> -->](longrightarrow.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | mapval2 6612* |
Alternate expression for the value of set exponentiation. (Contributed
by NM, 3-Nov-2007.)
|
![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![~P ~P](scrp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![{ {](lbrace.gif) ![B B](_cb.gif) ![} }](rbrace.gif) ![)
)](rp.gif) |
|
Theorem | elpm 6613 |
The predicate "is a partial function." (Contributed by NM,
15-Nov-2007.) (Revised by Mario Carneiro, 14-Nov-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif)
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elpm2 6614 |
The predicate "is a partial function." (Contributed by NM,
15-Nov-2007.) (Revised by Mario Carneiro, 31-Dec-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![F F](_cf.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fpm 6615 |
A total function is a partial function. (Contributed by NM,
15-Nov-2007.) (Revised by Mario Carneiro, 31-Dec-2013.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mapsspm 6616 |
Set exponentiation is a subset of partial maps. (Contributed by NM,
15-Nov-2007.) (Revised by Mario Carneiro, 27-Feb-2016.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | pmsspw 6617 |
Partial maps are a subset of the power set of the Cartesian product of
its arguments. (Contributed by Mario Carneiro, 2-Jan-2017.)
|
![( (](lp.gif) ![B B](_cb.gif) ![~P ~P](scrp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | mapsspw 6618 |
Set exponentiation is a subset of the power set of the Cartesian product
of its arguments. (Contributed by NM, 8-Dec-2006.) (Revised by Mario
Carneiro, 26-Apr-2015.)
|
![( (](lp.gif) ![B B](_cb.gif) ![~P ~P](scrp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | fvmptmap 6619* |
Special case of fvmpt 5538 for operator theorems. (Contributed by NM,
27-Nov-2007.)
|
![( (](lp.gif)
![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![B B](_cb.gif) ![( (](lp.gif) ![A A](_ca.gif) ![: :](colon.gif) ![D D](_cd.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | map0e 6620 |
Set exponentiation with an empty exponent (ordinal number 0) is ordinal
number 1. Exercise 4.42(a) of [Mendelson] p. 255. (Contributed by NM,
10-Dec-2003.) (Revised by Mario Carneiro, 30-Apr-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![(/) (/)](varnothing.gif) ![1o 1o](_1o.gif) ![) )](rp.gif) |
|
Theorem | map0b 6621 |
Set exponentiation with an empty base is the empty set, provided the
exponent is nonempty. Theorem 96 of [Suppes] p. 89. (Contributed by
NM, 10-Dec-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) |
|
Theorem | map0g 6622 |
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, 30-Apr-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | map0 6623 |
Set exponentiation is empty iff the base is empty and the exponent is
not empty. Theorem 97 of [Suppes] p. 89.
(Contributed by NM,
10-Dec-2003.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mapsn 6624* |
The value of set exponentiation with a singleton exponent. Theorem 98
of [Suppes] p. 89. (Contributed by NM,
10-Dec-2003.)
|
![( (](lp.gif) ![{ {](lbrace.gif) ![B B](_cb.gif) ![} }](rbrace.gif) ![{ {](lbrace.gif) ![E. E.](exists.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![B B](_cb.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![} }](rbrace.gif) |
|
Theorem | mapss 6625 |
Subset inheritance for set exponentiation. Theorem 99 of [Suppes]
p. 89. (Contributed by NM, 10-Dec-2003.) (Revised by Mario Carneiro,
26-Apr-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![C C](_cc.gif)
![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fdiagfn 6626* |
Functionality of the diagonal map. (Contributed by Stefan O'Rear,
24-Jan-2015.)
|
![( (](lp.gif) ![( (](lp.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) ![B B](_cb.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif)
![I I](_ci.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fvdiagfn 6627* |
Functionality of the diagonal map. (Contributed by Stefan O'Rear,
24-Jan-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![X X](_cx.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![X X](_cx.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mapsnconst 6628 |
Every singleton map is a constant function. (Contributed by Stefan
O'Rear, 25-Mar-2015.)
|
![{ {](lbrace.gif) ![X X](_cx.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif)
![( (](lp.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![X X](_cx.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | mapsncnv 6629* |
Expression for the inverse of the canonical map between a set and its
set of singleton functions. (Contributed by Stefan O'Rear,
21-Mar-2015.)
|
![{ {](lbrace.gif) ![X X](_cx.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![x x](_x.gif) ![` `](backtick.gif) ![X X](_cx.gif) ![) )](rp.gif) ![`' `'](_cnv.gif)
![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mapsnf1o2 6630* |
Explicit bijection between a set and its singleton functions.
(Contributed by Stefan O'Rear, 21-Mar-2015.)
|
![{ {](lbrace.gif) ![X X](_cx.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![x x](_x.gif) ![` `](backtick.gif) ![X X](_cx.gif) ![) )](rp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![B B](_cb.gif) |
|
Theorem | mapsnf1o3 6631* |
Explicit bijection in the reverse of mapsnf1o2 6630. (Contributed by
Stefan O'Rear, 24-Mar-2015.)
|
![{ {](lbrace.gif) ![X X](_cx.gif) ![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![B B](_cb.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) |
|
2.6.26 Infinite Cartesian products
|
|
Syntax | cixp 6632 |
Extend class notation to include infinite Cartesian products.
|
![X_ X_](_bigtimes.gif) ![B B](_cb.gif) |
|
Definition | df-ixp 6633* |
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 6634* |
Eliminate the expression ![{ {](lbrace.gif) ![A A](_ca.gif) in df-ixp 6633, 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 6635* |
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 6636* |
Membership in an infinite Cartesian product. See df-ixp 6633 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 6637* |
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 6638* |
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 6639* |
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 6640* |
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 6641* |
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 6642* |
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 6643* |
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 6644* |
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 6645 |
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 6646 |
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 6647* |
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 6648* |
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 6649* |
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 6650* |
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 6651* |
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 6652 |
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 6653* |
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 6654* |
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 6655* |
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 6656* |
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 6657* |
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 6658* |
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 6659* |
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 6660 |
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 6661* |
An infinite Cartesian product is a subset of set exponentiation. This
version of ixpssmapg 6662 avoids ax-coll 4075. (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 6662* |
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 6663 |
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 6664* |
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 6665 |
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 6666* |
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 6667* |
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 6668* |
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 6669* |
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 6670* |
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 6671* |
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 6672 |
Extend class definition to include the equinumerosity relation
("approximately equals" symbol)
|
![~~ ~~](approx.gif) |
|
Syntax | cdom 6673 |
Extend class definition to include the dominance relation (curly
less-than-or-equal)
|
![~<_ ~<_](preccurlyeq.gif) |
|
Syntax | cfn 6674 |
Extend class definition to include the class of all finite sets.
|
![Fin Fin](_fin.gif) |
|
Definition | df-en 6675* |
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 6681. (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 6676* |
Define the dominance relation. Compare Definition of [Enderton] p. 145.
Typical textbook definitions are derived as brdom 6684 and domen 6685.
(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 6677* |
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 13489. (Contributed by NM,
22-Aug-2008.)
|
![{ {](lbrace.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![} }](rbrace.gif) |
|
Theorem | relen 6678 |
Equinumerosity is a relation. (Contributed by NM, 28-Mar-1998.)
|
![~~ ~~](approx.gif) |
|
Theorem | reldom 6679 |
Dominance is a relation. (Contributed by NM, 28-Mar-1998.)
|
![~<_ ~<_](preccurlyeq.gif) |
|
Theorem | encv 6680 |
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 6681* |
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 6682* |
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 6683* |
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 6684* |
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 6685* |
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 6686* |
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 6687 |
A class dominated by is a set. See also ctfoex 7048 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 6688 |
The domain and range of a one-to-one, onto function are equinumerous.
This variation of f1oeng 6691 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 6689 |
The domain and range of a one-to-one, onto function are equinumerous.
This variation of f1oeng 6691 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 6690 |
The domain of a one-to-one function is dominated by its codomain. This
variation of f1domg 6692 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 6691 |
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 6692 |
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 6693 |
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 6694 |
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 6695* |
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 6696 |
Equinumerosity implies dominance. (Contributed by NM, 31-Mar-1998.)
|
![~<_ ~<_](preccurlyeq.gif) |
|
Theorem | endom 6697 |
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 6698 |
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 6699 |
Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed
by NM, 25-Sep-2004.)
|
![A A](_ca.gif) |
|
Theorem | eqeng 6700 |
Equality implies equinumerosity. (Contributed by NM, 26-Oct-2003.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |