P. 73 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 7201-7300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	domsdomtr 7201	Transitivity of dominance and strict dominance. Theorem 22(ii) of [Suppes] p. 97. (Contributed by NM, 10-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( ( A ~<_ B /\ B ~< C ) -> A ~< C )
Theorem	ensdomtr 7202	Transitivity of equinumerosity and strict dominance. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( ( A ~~ B /\ B ~< C ) -> A ~< C )
Theorem	sdomirr 7203	Strict dominance is irreflexive. Theorem 21(i) of [Suppes] p. 97. (Contributed by NM, 4-Jun-1998.)
|- -. A ~< A
Theorem	sdomtr 7204	Strict dominance is transitive. Theorem 21(iii) of [Suppes] p. 97. (Contributed by NM, 9-Jun-1998.)
|- ( ( A ~< B /\ B ~< C ) -> A ~< C )
Theorem	sdomn2lp 7205	Strict dominance has no 2-cycle loops. (Contributed by NM, 6-May-2008.)
|- -. ( A ~< B /\ B ~< A )
Theorem	enen1 7206	Equality-like theorem for equinumerosity. (Contributed by NM, 18-Dec-2003.)
|- ( A ~~ B -> ( A ~~ C <-> B ~~ C ) )
Theorem	enen2 7207	Equality-like theorem for equinumerosity. (Contributed by NM, 18-Dec-2003.)
|- ( A ~~ B -> ( C ~~ A <-> C ~~ B ) )
Theorem	domen1 7208	Equality-like theorem for equinumerosity and dominance. (Contributed by NM, 8-Nov-2003.)
|- ( A ~~ B -> ( A ~<_ C <-> B ~<_ C ) )
Theorem	domen2 7209	Equality-like theorem for equinumerosity and dominance. (Contributed by NM, 8-Nov-2003.)
|- ( A ~~ B -> ( C ~<_ A <-> C ~<_ B ) )
Theorem	sdomen1 7210	Equality-like theorem for equinumerosity and strict dominance. (Contributed by NM, 8-Nov-2003.)
|- ( A ~~ B -> ( A ~< C <-> B ~< C ) )
Theorem	sdomen2 7211	Equality-like theorem for equinumerosity and strict dominance. (Contributed by NM, 8-Nov-2003.)
|- ( A ~~ B -> ( C ~< A <-> C ~< B ) )
Theorem	domtriord 7212	Dominance is trichotomous in the restricted case of ordinal numbers. (Contributed by Jeff Hankins, 24-Oct-2009.)
|- ( ( A e. On /\ B e. On ) -> ( A ~<_ B <-> -. B ~< A ) )
Theorem	sdomel 7213	Strict dominance implies ordinal membership. (Contributed by Mario Carneiro, 13-Jan-2013.)
|- ( ( A e. On /\ B e. On ) -> ( A ~< B -> A e. B ) )
Theorem	sdomdif 7214	The difference of a set from a smaller set cannot be empty. (Contributed by Mario Carneiro, 5-Feb-2013.)
|- ( A ~< B -> ( B \ A ) =/= (/) )
Theorem	onsdominel 7215	An ordinal with more elements of some type is larger. (Contributed by Stefan O'Rear, 2-Nov-2014.)
|- ( ( A e. On /\ B e. On /\ ( A i^i C ) ~< ( B i^i C ) ) -> A e. B )
Theorem	domunsn 7216	Dominance over a set with one element added. (Contributed by Mario Carneiro, 18-May-2015.)
|- ( A ~< B -> ( A u. { C } ) ~<_ B )
Theorem	fodomr 7217*	There exists a mapping from a set onto any (non-empty) set that it dominates. (Contributed by NM, 23-Mar-2006.)
|- ( ( (/) ~< B /\ B ~<_ A ) -> E. f f : A -onto-> B )
Theorem	pwdom 7218	Injection of sets implies injection on power sets. (Contributed by Mario Carneiro, 9-Apr-2015.)
|- ( A ~<_ B -> ~P A ~<_ ~P B )
Theorem	canth2 7219	Cantor's Theorem. No set is equinumerous to its power set. Specifically, any set has a cardinality (size) strictly less than the cardinality of its power set. For example, the cardinality of real numbers is the same as the cardinality of the power set of integers, so real numbers cannot be put into a one-to-one correspondence with integers. Theorem 23 of [Suppes] p. 97. For the function version, see canth 6498. (Contributed by NM, 7-Aug-1994.)
|- A e. _V   =>    |- A ~< ~P A
Theorem	canth2g 7220	Cantor's theorem with the sethood requirement expressed as an antecedent. Theorem 23 of [Suppes] p. 97. (Contributed by NM, 7-Nov-2003.)
|- ( A e. V -> A ~< ~P A )
Theorem	2pwuninel 7221	The power set of the power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set. (Contributed by NM, 27-Jun-2008.)
|- -. ~P ~P U. A e. A
Theorem	2pwne 7222	No set equals the power set of its power set. (Contributed by NM, 17-Nov-2008.)
|- ( A e. V -> ~P ~P A =/= A )
Theorem	disjen 7223	A stronger form of pwuninel 6504. We can use pwuninel 6504, 2pwuninel 7221 to create one or two sets disjoint from a given set A, but here we show that in fact such constructions exist for arbitrarily large disjoint extensions, which is to say that for any set B we can construct a set x that is equinumerous to it and disjoint from A. (Contributed by Mario Carneiro, 7-Feb-2015.)
|- ( ( A e. V /\ B e. W ) -> ( ( A i^i ( B X. { ~P U. ran A } ) ) = (/) /\ ( B X. { ~P U. ran A } ) ~~ B ) )
Theorem	disjenex 7224*	Existence version of disjen 7223. (Contributed by Mario Carneiro, 7-Feb-2015.)
|- ( ( A e. V /\ B e. W ) -> E. x ( ( A i^i x ) = (/) /\ x ~~ B ) )
Theorem	domss2 7225	A corollary of disjenex 7224. If F is an injection from A to B then G is a right inverse of F from B to a superset of A. (Contributed by Mario Carneiro, 7-Feb-2015.) (Revised by Mario Carneiro, 24-Jun-2015.)
|- G = `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) )   =>    |- ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ( G : B -1-1-onto-> ran G /\ A C_ ran G /\ ( G o. F ) = ( _I |` A ) ) )
Theorem	domssex2 7226*	A corollary of disjenex 7224. If F is an injection from A to B then there is a right inverse g of F from B to a superset of A. (Contributed by Mario Carneiro, 7-Feb-2015.) (Revised by Mario Carneiro, 24-Jun-2015.)
|- ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> E. g ( g : B -1-1-> _V /\ ( g o. F ) = ( _I |` A ) ) )
Theorem	domssex 7227*	Weakening of domssex 7227 to forget the functions in favor of dominance and equinumerosity. (Contributed by Mario Carneiro, 7-Feb-2015.) (Revised by Mario Carneiro, 24-Jun-2015.)
|- ( A ~<_ B -> E. x ( A C_ x /\ B ~~ x ) )
2.4.33  Equinumerosity (cont.)
Theorem	xpf1o 7228*	Construct a bijection on a cross product given bijections on the factors. (Contributed by Mario Carneiro, 30-May-2015.)
|- ( ph -> ( x e. A |-> X ) : A -1-1-onto-> B )   &    |- ( ph -> ( y e. C |-> Y ) : C -1-1-onto-> D )   =>    |- ( ph -> ( x e. A , y e. C |-> <. X , Y >. ) : ( A X. C ) -1-1-onto-> ( B X. D ) )
Theorem	xpen 7229	Equinumerosity law for cross product. Proposition 4.22(b) of [Mendelson] p. 254. (Contributed by NM, 24-Jul-2004.) (Proof shortened by Mario Carneiro, 26-Apr-2015.)
|- ( ( A ~~ B /\ C ~~ D ) -> ( A X. C ) ~~ ( B X. D ) )
Theorem	mapen 7230	Two set exponentiations are equinumerous when their bases and exponents are equinumerous. Theorem 6H(c) of [Enderton] p. 139. (Contributed by NM, 16-Dec-2003.) (Proof shortened by Mario Carneiro, 26-Apr-2015.)
|- ( ( A ~~ B /\ C ~~ D ) -> ( A ^m C ) ~~ ( B ^m D ) )
Theorem	mapdom1 7231	Order-preserving property of set exponentiation. Theorem 6L(c) of [Enderton] p. 149. (Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro, 9-Mar-2013.)
|- ( A ~<_ B -> ( A ^m C ) ~<_ ( B ^m C ) )
Theorem	mapxpen 7232	Equinumerosity law for double set exponentiation. Proposition 10.45 of [TakeutiZaring] p. 96. (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 24-Jun-2015.)
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( ( A ^m B ) ^m C ) ~~ ( A ^m ( B X. C ) ) )
Theorem	xpmapenlem 7233*	Lemma for xpmapen 7234. (Contributed by NM, 1-May-2004.) (Revised by Mario Carneiro, 16-Nov-2014.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- D = ( z e. C |-> ( 1st ` ( x ` z ) ) )   &    |- R = ( z e. C |-> ( 2nd ` ( x ` z ) ) )   &    |- S = ( z e. C |-> <. ( ( 1st ` y ) ` z ) , ( ( 2nd ` y ) ` z ) >. )   =>    |- ( ( A X. B ) ^m C ) ~~ ( ( A ^m C ) X. ( B ^m C ) )
Theorem	xpmapen 7234	Equinumerosity law for set exponentiation of a cross product. Exercise 4.47 of [Mendelson] p. 255. (Contributed by NM, 23-Feb-2004.) (Proof shortened by Mario Carneiro, 16-Nov-2014.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   =>    |- ( ( A X. B ) ^m C ) ~~ ( ( A ^m C ) X. ( B ^m C ) )
Theorem	mapunen 7235	Equinumerosity law for set exponentiation of a disjoint union. Exercise 4.45 of [Mendelson] p. 255. (Contributed by NM, 23-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
|- ( ( ( A e. V /\ B e. W /\ C e. X ) /\ ( A i^i B ) = (/) ) -> ( C ^m ( A u. B ) ) ~~ ( ( C ^m A ) X. ( C ^m B ) ) )
Theorem	map2xp 7236	A cardinal power with exponent 2 is equivalent to a cross product with itself. (Contributed by Mario Carneiro, 31-May-2015.)
|- ( A e. V -> ( A ^m 2o ) ~~ ( A X. A ) )
Theorem	mapdom2 7237	Order-preserving property of set exponentiation. Theorem 6L(d) of [Enderton] p. 149. (Contributed by NM, 23-Sep-2004.) (Revised by Mario Carneiro, 30-Apr-2015.)
|- ( ( A ~<_ B /\ -. ( A = (/) /\ C = (/) ) ) -> ( C ^m A ) ~<_ ( C ^m B ) )
Theorem	mapdom3 7238	Set exponentiation dominates the mantissa. (Contributed by Mario Carneiro, 30-Apr-2015.)
|- ( ( A e. V /\ B e. W /\ B =/= (/) ) -> A ~<_ ( A ^m B ) )
Theorem	pwen 7239	If two sets are equinumerous, then their power sets are equinumerous. Proposition 10.15 of [TakeutiZaring] p. 87. (Contributed by NM, 29-Jan-2004.) (Revised by Mario Carneiro, 9-Apr-2015.)
|- ( A ~~ B -> ~P A ~~ ~P B )
Theorem	ssenen 7240*	Equinumerosity of equinumerous subsets of a set. (Contributed by NM, 30-Sep-2004.) (Revised by Mario Carneiro, 16-Nov-2014.)
|- ( A ~~ B -> { x | ( x C_ A /\ x ~~ C ) } ~~ { x | ( x C_ B /\ x ~~ C ) } )
Theorem	limenpsi 7241	A limit ordinal is equinumerous to a proper subset of itself. (Contributed by NM, 30-Oct-2003.) (Revised by Mario Carneiro, 16-Nov-2014.)
|- Lim A   =>    |- ( A e. V -> A ~~ ( A \ { (/) } ) )
Theorem	limensuci 7242	A limit ordinal is equinumerous to its successor. (Contributed by NM, 30-Oct-2003.)
|- Lim A   =>    |- ( A e. V -> A ~~ suc A )
Theorem	limensuc 7243	A limit ordinal is equinumerous to its successor. (Contributed by NM, 30-Oct-2003.)
|- ( ( A e. V /\ Lim A ) -> A ~~ suc A )
Theorem	infensuc 7244	Any infinite ordinal is equinumerous to its successor. Exercise 7 of [TakeutiZaring] p. 88. Proved without the Axiom of Infinity. (Contributed by NM, 30-Oct-2003.) (Revised by Mario Carneiro, 13-Jan-2013.)
|- ( ( A e. On /\ om C_ A ) -> A ~~ suc A )
2.4.34  Pigeonhole Principle
Theorem	phplem1 7245	Lemma for Pigeonhole Principle. If we join a natural number to itself minus an element, we end up with its successor minus the same element. (Contributed by NM, 25-May-1998.)
|- ( ( A e. om /\ B e. A ) -> ( { A } u. ( A \ { B } ) ) = ( suc A \ { B } ) )
Theorem	phplem2 7246	Lemma for Pigeonhole Principle. A natural number is equinumerous to its successor minus one of its elements. (Contributed by NM, 11-Jun-1998.) (Revised by Mario Carneiro, 16-Nov-2014.)
|- A e. _V   &    |- B e. _V   =>    |- ( ( A e. om /\ B e. A ) -> A ~~ ( suc A \ { B } ) )
Theorem	phplem3 7247	Lemma for Pigeonhole Principle. A natural number is equinumerous to its successor minus any element of the successor. (Contributed by NM, 26-May-1998.)
|- A e. _V   &    |- B e. _V   =>    |- ( ( A e. om /\ B e. suc A ) -> A ~~ ( suc A \ { B } ) )
Theorem	phplem4 7248	Lemma for Pigeonhole Principle. Equinumerosity of successors implies equinumerosity of the original natural numbers. (Contributed by NM, 28-May-1998.) (Revised by Mario Carneiro, 24-Jun-2015.)
|- A e. _V   &    |- B e. _V   =>    |- ( ( A e. om /\ B e. om ) -> ( suc A ~~ suc B -> A ~~ B ) )
Theorem	nneneq 7249	Two equinumerous natural numbers are equal. Proposition 10.20 of [TakeutiZaring] p. 90 and its converse. Also compare Corollary 6E of [Enderton] p. 136. (Contributed by NM, 28-May-1998.)
|- ( ( A e. om /\ B e. om ) -> ( A ~~ B <-> A = B ) )
Theorem	php 7250	Pigeonhole Principle. A natural number is not equinumerous to a proper subset of itself. Theorem (Pigeonhole Principle) of [Enderton] p. 134. The theorem is so-called because you can't put n + 1 pigeons into n holes (if each hole holds only one pigeon). The proof consists of lemmas phplem1 7245 through phplem4 7248, nneneq 7249, and this final piece of the proof. (Contributed by NM, 29-May-1998.)
|- ( ( A e. om /\ B C. A ) -> -. A ~~ B )
Theorem	php2 7251	Corollary of Pigeonhole Principle. (Contributed by NM, 31-May-1998.)
|- ( ( A e. om /\ B C. A ) -> B ~< A )
Theorem	php3 7252	Corollary of Pigeonhole Principle. If A is finite and B is a proper subset of A, the B is strictly less numerous than A. Stronger version of Corollary 6C of [Enderton] p. 135. (Contributed by NM, 22-Aug-2008.)
|- ( ( A e. Fin /\ B C. A ) -> B ~< A )
Theorem	php4 7253	Corollary of the Pigeonhole Principle php 7250: a natural number is strictly dominated by its successor. (Contributed by NM, 26-Jul-2004.)
|- ( A e. om -> A ~< suc A )
Theorem	php5 7254	Corollary of the Pigeonhole Principle php 7250: a natural number is not equinumerous to its successor. Corollary 10.21(1) of [TakeutiZaring] p. 90. (Contributed by NM, 26-Jul-2004.)
|- ( A e. om -> -. A ~~ suc A )
2.4.35  Finite sets
Theorem	onomeneq 7255	An ordinal number equinumerous to a natural number is equal to it. Proposition 10.22 of [TakeutiZaring] p. 90 and its converse. (Contributed by NM, 26-Jul-2004.)
|- ( ( A e. On /\ B e. om ) -> ( A ~~ B <-> A = B ) )
Theorem	onfin 7256	An ordinal number is finite iff it is a natural number. Proposition 10.32 of [TakeutiZaring] p. 92. (Contributed by NM, 26-Jul-2004.)
|- ( A e. On -> ( A e. Fin <-> A e. om ) )
Theorem	onfin2 7257	A set is a natural number iff it is a finite ordinal. (Contributed by Mario Carneiro, 22-Jan-2013.)
|- om = ( On i^i Fin )
Theorem	nnfi 7258	Natural numbers are finite sets. (Contributed by Stefan O'Rear, 21-Mar-2015.)
|- ( A e. om -> A e. Fin )
Theorem	nndomo 7259	Cardinal ordering agrees with natural number ordering. Example 3 of [Enderton] p. 146. (Contributed by NM, 17-Jun-1998.)
|- ( ( A e. om /\ B e. om ) -> ( A ~<_ B <-> A C_ B ) )
Theorem	nnsdomo 7260	Cardinal ordering agrees with natural number ordering. (Contributed by NM, 17-Jun-1998.)
|- ( ( A e. om /\ B e. om ) -> ( A ~< B <-> A C. B ) )
Theorem	omsucdomOLD 7261	Strict dominance of natural numbers is the same as dominance over the successor of the smaller. (Contributed by NM, 25-Jul-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( A e. om /\ B e. om ) -> ( A ~< B <-> suc A ~<_ B ) )
Theorem	sucdom2 7262	Strict dominance of a set over another set implies dominance over its successor. (Contributed by Mario Carneiro, 12-Jan-2013.) (Proof shortened by Mario Carneiro, 27-Apr-2015.)
|- ( A ~< B -> suc A ~<_ B )
Theorem	sucdom 7263	Strict dominance of a set over a natural number is the same as dominance over its successor. (Contributed by Mario Carneiro, 12-Jan-2013.)
|- ( A e. om -> ( A ~< B <-> suc A ~<_ B ) )
Theorem	sucdomiOLD 7264	Dominance of a set over a successor of a natural number implies strict dominance over the number. For the converse, see sucdom 7263. (Contributed by NM, 26-Jul-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( A e. om /\ B e. C ) -> ( suc A ~<_ B -> A ~< B ) )
Theorem	0sdom1dom 7265	Strict dominance over zero is the same as dominance over one. (Contributed by NM, 28-Sep-2004.)
|- ( (/) ~< A <-> 1o ~<_ A )
Theorem	1sdom2 7266	Ordinal 1 is strictly dominated by ordinal 2. (Contributed by NM, 4-Apr-2007.)
|- 1o ~< 2o
Theorem	sdom1 7267	A set has less than one member iff it is empty. (Contributed by Stefan O'Rear, 28-Oct-2014.)
|- ( A ~< 1o <-> A = (/) )
Theorem	modom 7268	Two ways to express "at most one". (Contributed by Stefan O'Rear, 28-Oct-2014.)
|- ( E* x ph <-> { x | ph } ~<_ 1o )
Theorem	modom2 7269*	Two ways to express "at most one". (Contributed by Mario Carneiro, 24-Dec-2016.)
|- ( E* x x e. A <-> A ~<_ 1o )
Theorem	1sdom 7270*	A set that strictly dominates ordinal 1 has at least 2 different members. (Closely related to 2dom 7138.) (Contributed by Mario Carneiro, 12-Jan-2013.)
|- ( A e. V -> ( 1o ~< A <-> E. x e. A E. y e. A -. x = y ) )
Theorem	fisucdomOLD 7271	Strict dominance of a finite set over a natural number is the same as dominance over its successor. (Contributed by NM, 26-Jul-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( A e. om /\ B e. Fin ) -> ( A ~< B <-> suc A ~<_ B ) )
Theorem	unxpdomlem1 7272*	Lemma for unxpdom 7275. (Trivial substitution proof.) (Contributed by Mario Carneiro, 13-Jan-2013.)
|- F = ( x e. ( a u. b ) |-> G )   &    |- G = if ( x e. a , <. x , if ( x = m , t , s ) >. , <. if ( x = t , n , m ) , x >. )   =>    |- ( z e. ( a u. b ) -> ( F ` z ) = if ( z e. a , <. z , if ( z = m , t , s ) >. , <. if ( z = t , n , m ) , z >. ) )
Theorem	unxpdomlem2 7273*	Lemma for unxpdom 7275. (Contributed by Mario Carneiro, 13-Jan-2013.)
|- F = ( x e. ( a u. b ) |-> G )   &    |- G = if ( x e. a , <. x , if ( x = m , t , s ) >. , <. if ( x = t , n , m ) , x >. )   &    |- ( ph -> w e. ( a u. b ) )   &    |- ( ph -> -. m = n )   &    |- ( ph -> -. s = t )   =>    |- ( ( ph /\ ( z e. a /\ -. w e. a ) ) -> -. ( F ` z ) = ( F ` w ) )
Theorem	unxpdomlem3 7274*	Lemma for unxpdom 7275. (Contributed by Mario Carneiro, 13-Jan-2013.) (Revised by Mario Carneiro, 16-Nov-2014.)
|- F = ( x e. ( a u. b ) |-> G )   &    |- G = if ( x e. a , <. x , if ( x = m , t , s ) >. , <. if ( x = t , n , m ) , x >. )   =>    |- ( ( 1o ~< a /\ 1o ~< b ) -> ( a u. b ) ~<_ ( a X. b ) )
Theorem	unxpdom 7275	Cross product dominates union for sets with cardinality greater than 1. Proposition 10.36 of [TakeutiZaring] p. 93. (Contributed by Mario Carneiro, 13-Jan-2013.) (Proof shortened by Mario Carneiro, 27-Apr-2015.)
|- ( ( 1o ~< A /\ 1o ~< B ) -> ( A u. B ) ~<_ ( A X. B ) )
Theorem	unxpdom2 7276	Corollary of unxpdom 7275. (Contributed by NM, 16-Sep-2004.)
|- ( ( 1o ~< A /\ B ~<_ A ) -> ( A u. B ) ~<_ ( A X. A ) )
Theorem	sucxpdom 7277	Cross product dominates successor for set with cardinality greater than 1. Proposition 10.38 of [TakeutiZaring] p. 93 (but generalized to arbitrary sets, not just ordinals). (Contributed by NM, 3-Sep-2004.) (Proof shortened by Mario Carneiro, 27-Apr-2015.)
|- ( 1o ~< A -> suc A ~<_ ( A X. A ) )
Theorem	pssinf 7278	A set equinumerous to a proper subset of itself is infinite. Corollary 6D(a) of [Enderton] p. 136. (Contributed by NM, 2-Jun-1998.)
|- ( ( A C. B /\ A ~~ B ) -> -. B e. Fin )
Theorem	fisseneq 7279	A finite set is equal to its subset if they are equinumerous. (Contributed by FL, 11-Aug-2008.)
|- ( ( B e. Fin /\ A C_ B /\ A ~~ B ) -> A = B )
Theorem	ominf 7280	The set of natural numbers is infinite. Corollary 6D(b) of [Enderton] p. 136. (Contributed by NM, 2-Jun-1998.)
|- -. om e. Fin
Theorem	isinf 7281*	Any set that is not finite is literally infinite, in the sense that it contains subsets of arbitrarily large finite cardinality. (It cannot be proven that the set has countably infinite subsets unless AC is invoked.) The proof does not require the Axiom of Infinity. (Contributed by Mario Carneiro, 15-Jan-2013.)
|- ( -. A e. Fin -> A. n e. om E. x ( x C_ A /\ x ~~ n ) )
Theorem	fineqvlem 7282	Lemma for fineqv 7283. (Contributed by Mario Carneiro, 20-Jan-2013.) (Proof shortened by Stefan O'Rear, 3-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)
|- ( ( A e. V /\ -. A e. Fin ) -> om ~<_ ~P ~P A )
Theorem	fineqv 7283	If the Axiom of Infinity is denied, then all sets are finite (which implies the Axiom of Choice). (Contributed by Mario Carneiro, 20-Jan-2013.) (Revised by Mario Carneiro, 3-Jan-2015.)
|- ( -. om e. _V <-> Fin = _V )
Theorem	enfi 7284	Equinmerous sets have the same finiteness. (Contributed by NM, 22-Aug-2008.)
|- ( A ~~ B -> ( A e. Fin <-> B e. Fin ) )
Theorem	enfii 7285	A set equinumerous to a finite set is finite. (Contributed by Mario Carneiro, 12-Mar-2015.)
|- ( ( B e. Fin /\ A ~~ B ) -> A e. Fin )
Theorem	pssnn 7286*	A proper subset of a natural number is equinumerous to some smaller number. Lemma 6F of [Enderton] p. 137. (Contributed by NM, 22-Jun-1998.) (Revised by Mario Carneiro, 16-Nov-2014.)
|- ( ( A e. om /\ B C. A ) -> E. x e. A B ~~ x )
Theorem	ssnnfi 7287	A subset of a natural number is finite. (Contributed by NM, 24-Jun-1998.)
|- ( ( A e. om /\ B C_ A ) -> B e. Fin )
Theorem	ssfi 7288	A subset of a finite set is finite. Corollary 6G of [Enderton] p. 138. (Contributed by NM, 24-Jun-1998.)
|- ( ( A e. Fin /\ B C_ A ) -> B e. Fin )
Theorem	domfi 7289	A set dominated by a finite set is finite. (Contributed by NM, 23-Mar-2006.) (Revised by Mario Carneiro, 12-Mar-2015.)
|- ( ( A e. Fin /\ B ~<_ A ) -> B e. Fin )
Theorem	xpfir 7290	The components of a non-empty finite cross product are finite. (Contributed by Paul Chapman, 11-Apr-2009.) (Proof shortened by Mario Carneiro, 29-Apr-2015.)
|- ( ( ( A X. B ) e. Fin /\ ( A X. B ) =/= (/) ) -> ( A e. Fin /\ B e. Fin ) )
Theorem	infi 7291	The interection of two sets is finite if one of them is. (Contributed by Thierry Arnoux, 14-Feb-2017.)
|- ( A e. Fin -> ( A i^i B ) e. Fin )
Theorem	rabfi 7292*	A restricted class built from a finite set is finite. (Contributed by Thierry Arnoux, 14-Feb-2017.)
|- ( A e. Fin -> { x e. A | ph } e. Fin )
Theorem	finresfin 7293	The restriction of a finite set is finite. (Contributed by Alexander van der Vekens, 3-Jan-2018.)
|- ( E e. Fin -> ( E |` B ) e. Fin )
Theorem	f1finf1o 7294	Any injection from one finite set to another of equal size must be a bijection. (Contributed by Jeff Madsen, 5-Jun-2010.) (Revised by Mario Carneiro, 27-Feb-2014.)
|- ( ( A ~~ B /\ B e. Fin ) -> ( F : A -1-1-> B <-> F : A -1-1-onto-> B ) )
Theorem	0fin 7295	The empty set is finite. (Contributed by FL, 14-Jul-2008.)
|- (/) e. Fin
Theorem	nfielex 7296*	If a class is not finite, it contains at least one element. (Contributed by Alexander van der Vekens, 12-Jan-2018.)
|- ( -. A e. Fin -> E. x x e. A )
Theorem	en1eqsn 7297	A set with one element is a singleton. (Contributed by FL, 18-Aug-2008.)
|- ( ( A e. B /\ B ~~ 1o ) -> B = { A } )
Theorem	diffi 7298	If A is finite, ( A \ B ) is finite. (Contributed by FL, 3-Aug-2009.)
|- ( A e. Fin -> ( A \ B ) e. Fin )
Theorem	dif1enOLD 7299	If a set A is equinumerous to the successor of a natural number M, then A with an element removed is equinumerous to M. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.)
|- A e. _V   =>    |- ( ( M e. om /\ A ~~ suc M /\ X e. A ) -> ( A \ { X } ) ~~ M )
Theorem	dif1en 7300	If a set A is equinumerous to the successor of a natural number M, then A with an element removed is equinumerous to M. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Stefan O'Rear, 16-Aug-2015.)
|- ( ( M e. om /\ A ~~ suc M /\ X e. A ) -> ( A \ { X } ) ~~ M )