P. 69 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6801-6900   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-dom 6801*	Define the dominance relation. Compare Definition of [Enderton] p. 145. Typical textbook definitions are derived as brdom 6809 and domen 6810. (Contributed by NM, 28-Mar-1998.)
|- ~<_ = { <. x , y >. | E. f f : x -1-1-> y }
Definition	df-fin 6802*	Define the (proper) class of all finite sets. Similar to Definition 10.29 of [TakeutiZaring] p. 91, whose "Fin(a)" corresponds to our " a e. Fin". This definition is meaningful whether or not we accept the Axiom of Infinity ax-inf2 15622. (Contributed by NM, 22-Aug-2008.)
|- Fin = { x | E. y e. om x ~~ y }
Theorem	relen 6803	Equinumerosity is a relation. (Contributed by NM, 28-Mar-1998.)
|- Rel ~~
Theorem	reldom 6804	Dominance is a relation. (Contributed by NM, 28-Mar-1998.)
|- Rel ~<_
Theorem	encv 6805	If two classes are equinumerous, both classes are sets. (Contributed by AV, 21-Mar-2019.)
|- ( A ~~ B -> ( A e. _V /\ B e. _V ) )
Theorem	bren 6806*	Equinumerosity relation. (Contributed by NM, 15-Jun-1998.)
|- ( A ~~ B <-> E. f f : A -1-1-onto-> B )
Theorem	brdomg 6807*	Dominance relation. (Contributed by NM, 15-Jun-1998.)
|- ( B e. C -> ( A ~<_ B <-> E. f f : A -1-1-> B ) )
Theorem	brdomi 6808*	Dominance relation. (Contributed by Mario Carneiro, 26-Apr-2015.)
|- ( A ~<_ B -> E. f f : A -1-1-> B )
Theorem	brdom 6809*	Dominance relation. (Contributed by NM, 15-Jun-1998.)
|- B e. _V   =>    |- ( A ~<_ B <-> E. f f : A -1-1-> B )
Theorem	domen 6810*	Dominance in terms of equinumerosity. Example 1 of [Enderton] p. 146. (Contributed by NM, 15-Jun-1998.)
|- B e. _V   =>    |- ( A ~<_ B <-> E. x ( A ~~ x /\ x C_ B ) )
Theorem	domeng 6811*	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.)
|- ( B e. C -> ( A ~<_ B <-> E. x ( A ~~ x /\ x C_ B ) ) )
Theorem	ctex 6812	A class dominated by om is a set. See also ctfoex 7184 which says that a countable class is a set. (Contributed by Thierry Arnoux, 29-Dec-2016.) (Proof shortened by Jim Kingdon, 13-Mar-2023.)
|- ( A ~<_ om -> A e. _V )
Theorem	f1oen3g 6813	The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng 6816 does not require the Axiom of Replacement. (Contributed by NM, 13-Jan-2007.) (Revised by Mario Carneiro, 10-Sep-2015.)
|- ( ( F e. V /\ F : A -1-1-onto-> B ) -> A ~~ B )
Theorem	f1oen2g 6814	The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng 6816 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( ( A e. V /\ B e. W /\ F : A -1-1-onto-> B ) -> A ~~ B )
Theorem	f1dom2g 6815	The domain of a one-to-one function is dominated by its codomain. This variation of f1domg 6817 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015.)
|- ( ( A e. V /\ B e. W /\ F : A -1-1-> B ) -> A ~<_ B )
Theorem	f1oeng 6816	The domain and range of a one-to-one, onto function are equinumerous. (Contributed by NM, 19-Jun-1998.)
|- ( ( A e. C /\ F : A -1-1-onto-> B ) -> A ~~ B )
Theorem	f1domg 6817	The domain of a one-to-one function is dominated by its codomain. (Contributed by NM, 4-Sep-2004.)
|- ( B e. C -> ( F : A -1-1-> B -> A ~<_ B ) )
Theorem	f1oen 6818	The domain and range of a one-to-one, onto function are equinumerous. (Contributed by NM, 19-Jun-1998.)
|- A e. _V   =>    |- ( F : A -1-1-onto-> B -> A ~~ B )
Theorem	f1dom 6819	The domain of a one-to-one function is dominated by its codomain. (Contributed by NM, 19-Jun-1998.)
|- B e. _V   =>    |- ( F : A -1-1-> B -> A ~<_ B )
Theorem	isfi 6820*	Express " A is finite". Definition 10.29 of [TakeutiZaring] p. 91 (whose " Fin " is a predicate instead of a class). (Contributed by NM, 22-Aug-2008.)
|- ( A e. Fin <-> E. x e. om A ~~ x )
Theorem	enssdom 6821	Equinumerosity implies dominance. (Contributed by NM, 31-Mar-1998.)
|- ~~ C_ ~<_
Theorem	endom 6822	Equinumerosity implies dominance. Theorem 15 of [Suppes] p. 94. (Contributed by NM, 28-May-1998.)
|- ( A ~~ B -> A ~<_ B )
Theorem	enrefg 6823	Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed by NM, 18-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( A e. V -> A ~~ A )
Theorem	enref 6824	Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed by NM, 25-Sep-2004.)
|- A e. _V   =>    |- A ~~ A
Theorem	eqeng 6825	Equality implies equinumerosity. (Contributed by NM, 26-Oct-2003.)
|- ( A e. V -> ( A = B -> A ~~ B ) )
Theorem	domrefg 6826	Dominance is reflexive. (Contributed by NM, 18-Jun-1998.)
|- ( A e. V -> A ~<_ A )
Theorem	en2d 6827*	Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro, 12-May-2014.)
|- ( ph -> A e. _V )   &    |- ( ph -> B e. _V )   &    |- ( ph -> ( x e. A -> C e. _V ) )   &    |- ( ph -> ( y e. B -> D e. _V ) )   &    |- ( ph -> ( ( x e. A /\ y = C ) <-> ( y e. B /\ x = D ) ) )   =>    |- ( ph -> A ~~ B )
Theorem	en3d 6828*	Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro, 12-May-2014.)
|- ( ph -> A e. _V )   &    |- ( ph -> B e. _V )   &    |- ( ph -> ( x e. A -> C e. B ) )   &    |- ( ph -> ( y e. B -> D e. A ) )   &    |- ( ph -> ( ( x e. A /\ y e. B ) -> ( x = D <-> y = C ) ) )   =>    |- ( ph -> A ~~ B )
Theorem	en2i 6829*	Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 4-Jan-2004.)
|- A e. _V   &    |- B e. _V   &    |- ( x e. A -> C e. _V )   &    |- ( y e. B -> D e. _V )   &    |- ( ( x e. A /\ y = C ) <-> ( y e. B /\ x = D ) )   =>    |- A ~~ B
Theorem	en3i 6830*	Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 19-Jul-2004.)
|- A e. _V   &    |- B e. _V   &    |- ( x e. A -> C e. B )   &    |- ( y e. B -> D e. A )   &    |- ( ( x e. A /\ y e. B ) -> ( x = D <-> y = C ) )   =>    |- A ~~ B
Theorem	dom2lem 6831*	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.)
|- ( ph -> ( x e. A -> C e. B ) )   &    |- ( ph -> ( ( x e. A /\ y e. A ) -> ( C = D <-> x = y ) ) )   =>    |- ( ph -> ( x e. A |-> C ) : A -1-1-> B )
Theorem	dom2d 6832*	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.)
|- ( ph -> ( x e. A -> C e. B ) )   &    |- ( ph -> ( ( x e. A /\ y e. A ) -> ( C = D <-> x = y ) ) )   =>    |- ( ph -> ( B e. R -> A ~<_ B ) )
Theorem	dom3d 6833*	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.)
|- ( ph -> ( x e. A -> C e. B ) )   &    |- ( ph -> ( ( x e. A /\ y e. A ) -> ( C = D <-> x = y ) ) )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. W )   =>    |- ( ph -> A ~<_ B )
Theorem	dom2 6834*	A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. C and D can be read C ( x ) and D ( y ), as can be inferred from their distinct variable conditions. (Contributed by NM, 26-Oct-2003.)
|- ( x e. A -> C e. B )   &    |- ( ( x e. A /\ y e. A ) -> ( C = D <-> x = y ) )   =>    |- ( B e. V -> A ~<_ B )
Theorem	dom3 6835*	A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. C and D can be read C ( x ) and D ( y ), as can be inferred from their distinct variable conditions. (Contributed by Mario Carneiro, 20-May-2013.)
|- ( x e. A -> C e. B )   &    |- ( ( x e. A /\ y e. A ) -> ( C = D <-> x = y ) )   =>    |- ( ( A e. V /\ B e. W ) -> A ~<_ B )
Theorem	idssen 6836	Equality implies equinumerosity. (Contributed by NM, 30-Apr-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- _I C_ ~~
Theorem	ssdomg 6837	A set dominates its subsets. Theorem 16 of [Suppes] p. 94. (Contributed by NM, 19-Jun-1998.) (Revised by Mario Carneiro, 24-Jun-2015.)
|- ( B e. V -> ( A C_ B -> A ~<_ B ) )
Theorem	ener 6838	Equinumerosity is an equivalence relation. (Contributed by NM, 19-Mar-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ~~ Er _V
Theorem	ensymb 6839	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by Mario Carneiro, 26-Apr-2015.)
|- ( A ~~ B <-> B ~~ A )
Theorem	ensym 6840	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( A ~~ B -> B ~~ A )
Theorem	ensymi 6841	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 25-Sep-2004.)
|- A ~~ B   =>    |- B ~~ A
Theorem	ensymd 6842	Symmetry of equinumerosity. Deduction form of ensym 6840. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A ~~ B )   =>    |- ( ph -> B ~~ A )
Theorem	entr 6843	Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92. (Contributed by NM, 9-Jun-1998.)
|- ( ( A ~~ B /\ B ~~ C ) -> A ~~ C )
Theorem	domtr 6844	Transitivity of dominance relation. Theorem 17 of [Suppes] p. 94. (Contributed by NM, 4-Jun-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A ~<_ B /\ B ~<_ C ) -> A ~<_ C )
Theorem	entri 6845	A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
|- A ~~ B   &    |- B ~~ C   =>    |- A ~~ C
Theorem	entr2i 6846	A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
|- A ~~ B   &    |- B ~~ C   =>    |- C ~~ A
Theorem	entr3i 6847	A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
|- A ~~ B   &    |- A ~~ C   =>    |- B ~~ C
Theorem	entr4i 6848	A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
|- A ~~ B   &    |- C ~~ B   =>    |- A ~~ C
Theorem	endomtr 6849	Transitivity of equinumerosity and dominance. (Contributed by NM, 7-Jun-1998.)
|- ( ( A ~~ B /\ B ~<_ C ) -> A ~<_ C )
Theorem	domentr 6850	Transitivity of dominance and equinumerosity. (Contributed by NM, 7-Jun-1998.)
|- ( ( A ~<_ B /\ B ~~ C ) -> A ~<_ C )
Theorem	f1imaeng 6851	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.)
|- ( ( F : A -1-1-> B /\ C C_ A /\ C e. V ) -> ( F " C ) ~~ C )
Theorem	f1imaen2g 6852	A one-to-one function's image under a subset of its domain is equinumerous to the subset. (This version of f1imaen 6853 does not need ax-setind 4573.) (Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro, 25-Jun-2015.)
|- ( ( ( F : A -1-1-> B /\ B e. V ) /\ ( C C_ A /\ C e. V ) ) -> ( F " C ) ~~ C )
Theorem	f1imaen 6853	A one-to-one function's image under a subset of its domain is equinumerous to the subset. (Contributed by NM, 30-Sep-2004.)
|- C e. _V   =>    |- ( ( F : A -1-1-> B /\ C C_ A ) -> ( F " C ) ~~ C )
Theorem	en0 6854	The empty set is equinumerous only to itself. Exercise 1 of [TakeutiZaring] p. 88. (Contributed by NM, 27-May-1998.)
|- ( A ~~ (/) <-> A = (/) )
Theorem	ensn1 6855	A singleton is equinumerous to ordinal one. (Contributed by NM, 4-Nov-2002.)
|- A e. _V   =>    |- { A } ~~ 1o
Theorem	ensn1g 6856	A singleton is equinumerous to ordinal one. (Contributed by NM, 23-Apr-2004.)
|- ( A e. V -> { A } ~~ 1o )
Theorem	enpr1g 6857	{ A , A } has only one element. (Contributed by FL, 15-Feb-2010.)
|- ( A e. V -> { A , A } ~~ 1o )
Theorem	en1 6858*	A set is equinumerous to ordinal one iff it is a singleton. (Contributed by NM, 25-Jul-2004.)
|- ( A ~~ 1o <-> E. x A = { x } )
Theorem	en1bg 6859	A set is equinumerous to ordinal one iff it is a singleton. (Contributed by Jim Kingdon, 13-Apr-2020.)
|- ( A e. V -> ( A ~~ 1o <-> A = { U. A } ) )
Theorem	reuen1 6860*	Two ways to express "exactly one". (Contributed by Stefan O'Rear, 28-Oct-2014.)
|- ( E! x e. A ph <-> { x e. A | ph } ~~ 1o )
Theorem	euen1 6861	Two ways to express "exactly one". (Contributed by Stefan O'Rear, 28-Oct-2014.)
|- ( E! x ph <-> { x | ph } ~~ 1o )
Theorem	euen1b 6862*	Two ways to express " A has a unique element". (Contributed by Mario Carneiro, 9-Apr-2015.)
|- ( A ~~ 1o <-> E! x x e. A )
Theorem	en1uniel 6863	A singleton contains its sole element. (Contributed by Stefan O'Rear, 16-Aug-2015.)
|- ( S ~~ 1o -> U. S e. S )
Theorem	2dom 6864*	A set that dominates ordinal 2 has at least 2 different members. (Contributed by NM, 25-Jul-2004.)
|- ( 2o ~<_ A -> E. x e. A E. y e. A -. x = y )
Theorem	fundmen 6865	A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98. (Contributed by NM, 28-Jul-2004.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- F e. _V   =>    |- ( Fun F -> dom F ~~ F )
Theorem	fundmeng 6866	A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98. (Contributed by NM, 17-Sep-2013.)
|- ( ( F e. V /\ Fun F ) -> dom F ~~ F )
Theorem	cnven 6867	A relational set is equinumerous to its converse. (Contributed by Mario Carneiro, 28-Dec-2014.)
|- ( ( Rel A /\ A e. V ) -> A ~~ `' A )
Theorem	cnvct 6868	If a set is dominated by om, so is its converse. (Contributed by Thierry Arnoux, 29-Dec-2016.)
|- ( A ~<_ om -> `' A ~<_ om )
Theorem	fndmeng 6869	A function is equinumerate to its domain. (Contributed by Paul Chapman, 22-Jun-2011.)
|- ( ( F Fn A /\ A e. C ) -> A ~~ F )
Theorem	mapsnen 6870	Set exponentiation to a singleton exponent is equinumerous to its base. Exercise 4.43 of [Mendelson] p. 255. (Contributed by NM, 17-Dec-2003.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- A e. _V   &    |- B e. _V   =>    |- ( A ^m { B } ) ~~ A
Theorem	map1 6871	Set exponentiation: ordinal 1 to any set is equinumerous to ordinal 1. Exercise 4.42(b) of [Mendelson] p. 255. (Contributed by NM, 17-Dec-2003.)
|- ( A e. V -> ( 1o ^m A ) ~~ 1o )
Theorem	en2sn 6872	Two singletons are equinumerous. (Contributed by NM, 9-Nov-2003.)
|- ( ( A e. C /\ B e. D ) -> { A } ~~ { B } )
Theorem	snfig 6873	A singleton is finite. For the proper class case, see snprc 3687. (Contributed by Jim Kingdon, 13-Apr-2020.)
|- ( A e. V -> { A } e. Fin )
Theorem	fiprc 6874	The class of finite sets is a proper class. (Contributed by Jeff Hankins, 3-Oct-2008.)
|- Fin e/ _V
Theorem	unen 6875	Equinumerosity of union of disjoint sets. Theorem 4 of [Suppes] p. 92. (Contributed by NM, 11-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( ( ( A ~~ B /\ C ~~ D ) /\ ( ( A i^i C ) = (/) /\ ( B i^i D ) = (/) ) ) -> ( A u. C ) ~~ ( B u. D ) )
Theorem	enpr2d 6876	A pair with distinct elements is equinumerous to ordinal two. (Contributed by Rohan Ridenour, 3-Aug-2023.)
|- ( ph -> A e. C )   &    |- ( ph -> B e. D )   &    |- ( ph -> -. A = B )   =>    |- ( ph -> { A , B } ~~ 2o )
Theorem	ssct 6877	A subset of a set dominated by om is dominated by om. (Contributed by Thierry Arnoux, 31-Jan-2017.)
|- ( ( A C_ B /\ B ~<_ om ) -> A ~<_ om )
Theorem	1domsn 6878	A singleton (whether of a set or a proper class) is dominated by one. (Contributed by Jim Kingdon, 1-Mar-2022.)
|- { A } ~<_ 1o
Theorem	enm 6879*	A set equinumerous to an inhabited set is inhabited. (Contributed by Jim Kingdon, 19-May-2020.)
|- ( ( A ~~ B /\ E. x x e. A ) -> E. y y e. B )
Theorem	xpsnen 6880	A set is equinumerous to its Cartesian product with a singleton. Proposition 4.22(c) of [Mendelson] p. 254. (Contributed by NM, 4-Jan-2004.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- A e. _V   &    |- B e. _V   =>    |- ( A X. { B } ) ~~ A
Theorem	xpsneng 6881	A set is equinumerous to its Cartesian product with a singleton. Proposition 4.22(c) of [Mendelson] p. 254. (Contributed by NM, 22-Oct-2004.)
|- ( ( A e. V /\ B e. W ) -> ( A X. { B } ) ~~ A )
Theorem	xp1en 6882	One times a cardinal number. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
|- ( A e. V -> ( A X. 1o ) ~~ A )
Theorem	endisj 6883*	Any two sets are equinumerous to disjoint sets. Exercise 4.39 of [Mendelson] p. 255. (Contributed by NM, 16-Apr-2004.)
|- A e. _V   &    |- B e. _V   =>    |- E. x E. y ( ( x ~~ A /\ y ~~ B ) /\ ( x i^i y ) = (/) )
Theorem	xpcomf1o 6884*	The canonical bijection from ( A X. B ) to ( B X. A ). (Contributed by Mario Carneiro, 23-Apr-2014.)
|- F = ( x e. ( A X. B ) |-> U. `' { x } )   =>    |- F : ( A X. B ) -1-1-onto-> ( B X. A )
Theorem	xpcomco 6885*	Composition with the bijection of xpcomf1o 6884 swaps the arguments to a mapping. (Contributed by Mario Carneiro, 30-May-2015.)
|- F = ( x e. ( A X. B ) |-> U. `' { x } )   &    |- G = ( y e. B , z e. A |-> C )   =>    |- ( G o. F ) = ( z e. A , y e. B |-> C )
Theorem	xpcomen 6886	Commutative law for equinumerosity of Cartesian product. Proposition 4.22(d) of [Mendelson] p. 254. (Contributed by NM, 5-Jan-2004.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- A e. _V   &    |- B e. _V   =>    |- ( A X. B ) ~~ ( B X. A )
Theorem	xpcomeng 6887	Commutative law for equinumerosity of Cartesian product. Proposition 4.22(d) of [Mendelson] p. 254. (Contributed by NM, 27-Mar-2006.)
|- ( ( A e. V /\ B e. W ) -> ( A X. B ) ~~ ( B X. A ) )
Theorem	xpsnen2g 6888	A set is equinumerous to its Cartesian product with a singleton on the left. (Contributed by Stefan O'Rear, 21-Nov-2014.)
|- ( ( A e. V /\ B e. W ) -> ( { A } X. B ) ~~ B )
Theorem	xpassen 6889	Associative law for equinumerosity of Cartesian product. Proposition 4.22(e) of [Mendelson] p. 254. (Contributed by NM, 22-Jan-2004.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   =>    |- ( ( A X. B ) X. C ) ~~ ( A X. ( B X. C ) )
Theorem	xpdom2 6890	Dominance law for Cartesian product. Proposition 10.33(2) of [TakeutiZaring] p. 92. (Contributed by NM, 24-Jul-2004.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- C e. _V   =>    |- ( A ~<_ B -> ( C X. A ) ~<_ ( C X. B ) )
Theorem	xpdom2g 6891	Dominance law for Cartesian product. Theorem 6L(c) of [Enderton] p. 149. (Contributed by Mario Carneiro, 26-Apr-2015.)
|- ( ( C e. V /\ A ~<_ B ) -> ( C X. A ) ~<_ ( C X. B ) )
Theorem	xpdom1g 6892	Dominance law for Cartesian product. Theorem 6L(c) of [Enderton] p. 149. (Contributed by NM, 25-Mar-2006.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( ( C e. V /\ A ~<_ B ) -> ( A X. C ) ~<_ ( B X. C ) )
Theorem	xpdom3m 6893*	A set is dominated by its Cartesian product with an inhabited set. Exercise 6 of [Suppes] p. 98. (Contributed by Jim Kingdon, 15-Apr-2020.)
|- ( ( A e. V /\ B e. W /\ E. x x e. B ) -> A ~<_ ( A X. B ) )
Theorem	xpdom1 6894	Dominance law for Cartesian product. Theorem 6L(c) of [Enderton] p. 149. (Contributed by NM, 28-Sep-2004.) (Revised by NM, 29-Mar-2006.) (Revised by Mario Carneiro, 7-May-2015.)
|- C e. _V   =>    |- ( A ~<_ B -> ( A X. C ) ~<_ ( B X. C ) )
Theorem	pw2f1odclem 6895*	Lemma for pw2f1odc 6896. (Contributed by Mario Carneiro, 6-Oct-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. W )   &    |- ( ph -> B =/= C )   &    |- ( ph -> A. p e. A A. q e. ~P ADECID p e. q )   =>    |- ( ph -> ( ( S e. ~P A /\ G = ( z e. A |-> if ( z e. S , C , B ) ) ) <-> ( G e. ( { B , C } ^m A ) /\ S = ( `' G " { C } ) ) ) )
Theorem	pw2f1odc 6896*	The power set of a set is equinumerous to set exponentiation with an unordered pair base of ordinal 2. Generalized from Proposition 10.44 of [TakeutiZaring] p. 96. (Contributed by Mario Carneiro, 6-Oct-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. W )   &    |- ( ph -> B =/= C )   &    |- ( ph -> A. p e. A A. q e. ~P ADECID p e. q )   &    |- F = ( x e. ~P A |-> ( z e. A |-> if ( z e. x , C , B ) ) )   =>    |- ( ph -> F : ~P A -1-1-onto-> ( { B , C } ^m A ) )
Theorem	fopwdom 6897	Covering implies injection on power sets. (Contributed by Stefan O'Rear, 6-Nov-2014.) (Revised by Mario Carneiro, 24-Jun-2015.)
|- ( ( F e. _V /\ F : A -onto-> B ) -> ~P B ~<_ ~P A )
Theorem	0domg 6898	Any set dominates the empty set. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( A e. V -> (/) ~<_ A )
Theorem	dom0 6899	A set dominated by the empty set is empty. (Contributed by NM, 22-Nov-2004.)
|- ( A ~<_ (/) <-> A = (/) )
Theorem	0dom 6900	Any set dominates the empty set. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- A e. _V   =>    |- (/) ~<_ A