P. 88 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 8701-8800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cfsmo 8701*	The map in cff1 8688 can be assumed to be a strictly monotone ordinal function without loss of generality. (Contributed by Mario Carneiro, 28-Feb-2013.)
|- ( A e. On -> E. f ( f : ( cf ` A ) --> A /\ Smo f /\ A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) ) )
Theorem	cfcoflem 8702*	Lemma for cfcof 8704, showing subset relation in one direction. (Contributed by Mario Carneiro, 9-Mar-2013.) (Revised by Mario Carneiro, 26-Dec-2014.)
|- ( ( A e. On /\ B e. On ) -> ( E. f ( f : B --> A /\ Smo f /\ A. x e. A E. y e. B x C_ ( f ` y ) ) -> ( cf ` A ) C_ ( cf ` B ) ) )
Theorem	coftr 8703*	If there is a cofinal map from B to A and another from C to A, then there is also a cofinal map from C to B. Proposition 11.9 of [TakeutiZaring] p. 102. A limited form of transitivity for the "cof" relation. This is really a lemma for cfcof 8704. (Contributed by Mario Carneiro, 16-Mar-2013.)
|- H = ( t e. C |-> |^| { n e. B | ( g ` t ) C_ ( f ` n ) } )   =>    |- ( E. f ( f : B --> A /\ Smo f /\ A. x e. A E. y e. B x C_ ( f ` y ) ) -> ( E. g ( g : C --> A /\ A. z e. A E. w e. C z C_ ( g ` w ) ) -> E. h ( h : C --> B /\ A. s e. B E. w e. C s C_ ( h ` w ) ) ) )
Theorem	cfcof 8704*	If there is a cofinal map from A to B, then they have the same cofinality. This was used as Definition 11.1 of [TakeutiZaring] p. 100, who defines an equivalence relation cof ( A , B ) and defines our cf ( B ) as the minimum B such that cof ( A , B ). (Contributed by Mario Carneiro, 20-Mar-2013.)
|- ( ( A e. On /\ B e. On ) -> ( E. f ( f : B --> A /\ Smo f /\ A. z e. A E. w e. B z C_ ( f ` w ) ) -> ( cf ` A ) = ( cf ` B ) ) )
Theorem	cfidm 8705	The cofinality function is idempotent. (Contributed by Mario Carneiro, 7-Mar-2013.) (Revised by Mario Carneiro, 15-Sep-2013.)
|- ( cf ` ( cf ` A ) ) = ( cf ` A )
Theorem	alephsing 8706	The cofinality of a limit aleph is the same as the cofinality of its argument, so if ( aleph ` A ) < A, then ( aleph ` A ) is singular. Conversely, if ( aleph ` A ) is regular (i.e. weakly inaccessible), then ( aleph ` A ) = A, so A has to be rather large (see alephfp 8539). Proposition 11.13 of [TakeutiZaring] p. 103. (Contributed by Mario Carneiro, 9-Mar-2013.)
|- ( Lim A -> ( cf ` ( aleph ` A ) ) = ( cf ` A ) )
2.6.12  Eight inequivalent definitions of finite set
Theorem	sornom 8707*	The range of a single-step monotone function from om into a partially ordered set is a chain. (Contributed by Stefan O'Rear, 3-Nov-2014.)
|- ( ( F Fn om /\ A. a e. om ( ( F ` a ) R ( F ` suc a ) \/ ( F ` a ) = ( F ` suc a ) ) /\ R Po ran F ) -> R Or ran F )
Syntax	cfin1a 8708	Extend class notation to include the class of Ia-finite sets.
class FinIa
Syntax	cfin2 8709	Extend class notation to include the class of II-finite sets.
class FinII
Syntax	cfin4 8710	Extend class notation to include the class of IV-finite sets.
class FinIV
Syntax	cfin3 8711	Extend class notation to include the class of III-finite sets.
class FinIII
Syntax	cfin5 8712	Extend class notation to include the class of V-finite sets.
class FinV
Syntax	cfin6 8713	Extend class notation to include the class of VI-finite sets.
class FinVI
Syntax	cfin7 8714	Extend class notation to include the class of VII-finite sets.
class FinVII
Definition	df-fin1a 8715*	A set is Ia-finite iff it is not the union of two I-infinite sets. Equivalent to definition Ia of [Levy58] p. 2. A I-infinite Ia-finite set is also known as an amorphous set. This is the second of Levy's eight definitions of finite set. Levy's I-finite is equivalent to our df-fin 7573 and not repeated here. These eight definitions are equivalent with Choice but strictly decreasing in strength in models where Choice fails; conversely, they provide a series of increasingly stronger notions of infiniteness. (Contributed by Stefan O'Rear, 12-Nov-2014.)
|- FinIa = { x | A. y e. ~P x ( y e. Fin \/ ( x \ y ) e. Fin ) }
Definition	df-fin2 8716*	A set is II-finite (Tarski finite) iff every nonempty chain of subsets contains a maximum element. Definition II of [Levy58] p. 2. (Contributed by Stefan O'Rear, 12-Nov-2014.)
|- FinII = { x | A. y e. ~P ~P x ( ( y =/= (/) /\ [ C.] Or y ) -> U. y e. y ) }
Definition	df-fin4 8717*	A set is IV-finite (Dedekind finite) iff it has no equinumerous proper subset. Definition IV of [Levy58] p. 3. (Contributed by Stefan O'Rear, 12-Nov-2014.)
|- FinIV = { x | -. E. y ( y C. x /\ y ~~ x ) }
Definition	df-fin3 8718	A set is III-finite (weakly Dedekind finite) iff its power set is Dedekind finite. Definition III of [Levy58] p. 2. (Contributed by Stefan O'Rear, 12-Nov-2014.)
|- FinIII = { x | ~P x e. FinIV }
Definition	df-fin5 8719	A set is V-finite iff it behaves finitely under +c. Definition V of [Levy58] p. 3. (Contributed by Stefan O'Rear, 12-Nov-2014.)
|- FinV = { x | ( x = (/) \/ x ~< ( x +c x ) ) }
Definition	df-fin6 8720	A set is VI-finite iff it behaves finitely under X.. Definition VI of [Levy58] p. 4. (Contributed by Stefan O'Rear, 12-Nov-2014.)
|- FinVI = { x | ( x ~< 2o \/ x ~< ( x X. x ) ) }
Definition	df-fin7 8721*	A set is VII-finite iff it cannot be infinitely well-ordered. Equivalent to definition VII of [Levy58] p. 4. (Contributed by Stefan O'Rear, 12-Nov-2014.)
|- FinVII = { x | -. E. y e. ( On \ om ) x ~~ y }
Theorem	isfin1a 8722*	Definition of a Ia-finite set. (Contributed by Stefan O'Rear, 16-May-2015.)
|- ( A e. V -> ( A e. FinIa <-> A. y e. ~P A ( y e. Fin \/ ( A \ y ) e. Fin ) ) )
Theorem	fin1ai 8723	Property of a Ia-finite set. (Contributed by Stefan O'Rear, 16-May-2015.)
|- ( ( A e. FinIa /\ X C_ A ) -> ( X e. Fin \/ ( A \ X ) e. Fin ) )
Theorem	isfin2 8724*	Definition of a II-finite set. (Contributed by Stefan O'Rear, 16-May-2015.)
|- ( A e. V -> ( A e. FinII <-> A. y e. ~P ~P A ( ( y =/= (/) /\ [ C.] Or y ) -> U. y e. y ) ) )
Theorem	fin2i 8725	Property of a II-finite set. (Contributed by Stefan O'Rear, 16-May-2015.)
|- ( ( ( A e. FinII /\ B C_ ~P A ) /\ ( B =/= (/) /\ [ C.] Or B ) ) -> U. B e. B )
Theorem	isfin3 8726	Definition of a III-finite set. (Contributed by Stefan O'Rear, 16-May-2015.)
|- ( A e. FinIII <-> ~P A e. FinIV )
Theorem	isfin4 8727*	Definition of a IV-finite set. (Contributed by Stefan O'Rear, 16-May-2015.)
|- ( A e. V -> ( A e. FinIV <-> -. E. y ( y C. A /\ y ~~ A ) ) )
Theorem	fin4i 8728	Infer that a set is IV-infinite. (Contributed by Stefan O'Rear, 16-May-2015.)
|- ( ( X C. A /\ X ~~ A ) -> -. A e. FinIV )
Theorem	isfin5 8729	Definition of a V-finite set. (Contributed by Stefan O'Rear, 16-May-2015.)
|- ( A e. FinV <-> ( A = (/) \/ A ~< ( A +c A ) ) )
Theorem	isfin6 8730	Definition of a VI-finite set. (Contributed by Stefan O'Rear, 16-May-2015.)
|- ( A e. FinVI <-> ( A ~< 2o \/ A ~< ( A X. A ) ) )
Theorem	isfin7 8731*	Definition of a VII-finite set. (Contributed by Stefan O'Rear, 16-May-2015.)
|- ( A e. V -> ( A e. FinVII <-> -. E. y e. ( On \ om ) A ~~ y ) )
Theorem	sdom2en01 8732	A set with less than two elements has 0 or 1. (Contributed by Stefan O'Rear, 30-Oct-2014.)
|- ( A ~< 2o <-> ( A = (/) \/ A ~~ 1o ) )
Theorem	infpssrlem1 8733	Lemma for infpssr 8738. (Contributed by Stefan O'Rear, 30-Oct-2014.)
|- ( ph -> B C_ A )   &    |- ( ph -> F : B -1-1-onto-> A )   &    |- ( ph -> C e. ( A \ B ) )   &    |- G = ( rec ( `' F , C ) |` om )   =>    |- ( ph -> ( G ` (/) ) = C )
Theorem	infpssrlem2 8734	Lemma for infpssr 8738. (Contributed by Stefan O'Rear, 30-Oct-2014.)
|- ( ph -> B C_ A )   &    |- ( ph -> F : B -1-1-onto-> A )   &    |- ( ph -> C e. ( A \ B ) )   &    |- G = ( rec ( `' F , C ) |` om )   =>    |- ( M e. om -> ( G ` suc M ) = ( `' F ` ( G ` M ) ) )
Theorem	infpssrlem3 8735	Lemma for infpssr 8738. (Contributed by Stefan O'Rear, 30-Oct-2014.)
|- ( ph -> B C_ A )   &    |- ( ph -> F : B -1-1-onto-> A )   &    |- ( ph -> C e. ( A \ B ) )   &    |- G = ( rec ( `' F , C ) |` om )   =>    |- ( ph -> G : om --> A )
Theorem	infpssrlem4 8736	Lemma for infpssr 8738. (Contributed by Stefan O'Rear, 30-Oct-2014.)
|- ( ph -> B C_ A )   &    |- ( ph -> F : B -1-1-onto-> A )   &    |- ( ph -> C e. ( A \ B ) )   &    |- G = ( rec ( `' F , C ) |` om )   =>    |- ( ( ph /\ M e. om /\ N e. M ) -> ( G ` M ) =/= ( G ` N ) )
Theorem	infpssrlem5 8737	Lemma for infpssr 8738. (Contributed by Stefan O'Rear, 30-Oct-2014.)
|- ( ph -> B C_ A )   &    |- ( ph -> F : B -1-1-onto-> A )   &    |- ( ph -> C e. ( A \ B ) )   &    |- G = ( rec ( `' F , C ) |` om )   =>    |- ( ph -> ( A e. V -> om ~<_ A ) )
Theorem	infpssr 8738	Dedekind infinity implies existence of a denumerable subset: take a single point witnessing the proper subset relation and iterate the embedding. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Revised by Mario Carneiro, 16-May-2015.)
|- ( ( X C. A /\ X ~~ A ) -> om ~<_ A )
Theorem	fin4en1 8739	Dedekind finite is a cardinal property. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Revised by Mario Carneiro, 16-May-2015.)
|- ( A ~~ B -> ( A e. FinIV -> B e. FinIV ) )
Theorem	ssfin4 8740	Dedekind finite sets have Dedekind finite subsets. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Revised by Mario Carneiro, 16-May-2015.) (Revised by Mario Carneiro, 6-May-2015.)
|- ( ( A e. FinIV /\ B C_ A ) -> B e. FinIV )
Theorem	domfin4 8741	A set dominated by a Dedekind finite set is Dedekind finite. (Contributed by Mario Carneiro, 16-May-2015.)
|- ( ( A e. FinIV /\ B ~<_ A ) -> B e. FinIV )
Theorem	ominf4 8742	om is Dedekind infinite. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Proof shortened by Mario Carneiro, 16-May-2015.)
|- -. om e. FinIV
Theorem	infpssALT 8743*	Alternate proof of infpss 8647, shorter but requiring Replacement (ax-rep 4515). (Contributed by Stefan O'Rear, 30-Oct-2014.) (Revised by Mario Carneiro, 16-May-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( om ~<_ A -> E. x ( x C. A /\ x ~~ A ) )
Theorem	isfin4-2 8744	Alternate definition of IV-finite sets: they lack a denumerable subset. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Revised by Mario Carneiro, 17-May-2015.)
|- ( A e. V -> ( A e. FinIV <-> -. om ~<_ A ) )
Theorem	isfin4-3 8745	Alternate definition of IV-finite sets: they are strictly dominated by their successors. (Thus, the proper subset referred to in isfin4 8727 can be assumed to be only a singleton smaller than the original.) (Contributed by Mario Carneiro, 18-May-2015.)
|- ( A e. FinIV <-> A ~< ( A +c 1o ) )
Theorem	fin23lem7 8746*	Lemma for isfin2-2 8749. The componentwise complement of a nonempty collection of sets is nonempty. (Contributed by Stefan O'Rear, 31-Oct-2014.) (Revised by Mario Carneiro, 16-May-2015.)
|- ( ( A e. V /\ B C_ ~P A /\ B =/= (/) ) -> { x e. ~P A | ( A \ x ) e. B } =/= (/) )
Theorem	fin23lem11 8747*	Lemma for isfin2-2 8749. (Contributed by Stefan O'Rear, 31-Oct-2014.) (Revised by Mario Carneiro, 16-May-2015.)
|- ( z = ( A \ x ) -> ( ps <-> ch ) )   &    |- ( w = ( A \ v ) -> ( ph <-> th ) )   &    |- ( ( x C_ A /\ v C_ A ) -> ( ch <-> th ) )   =>    |- ( B C_ ~P A -> ( E. x e. { c e. ~P A | ( A \ c ) e. B } A. w e. { c e. ~P A | ( A \ c ) e. B } -. ph -> E. z e. B A. v e. B -. ps ) )
Theorem	fin2i2 8748	A II-finite set contains minimal elements for every nonempty chain. (Contributed by Mario Carneiro, 16-May-2015.)
|- ( ( ( A e. FinII /\ B C_ ~P A ) /\ ( B =/= (/) /\ [ C.] Or B ) ) -> |^| B e. B )
Theorem	isfin2-2 8749*	FinII expressed in terms of minimal elements. (Contributed by Stefan O'Rear, 2-Nov-2014.) (Proof shortened by Mario Carneiro, 16-May-2015.)
|- ( A e. V -> ( A e. FinII <-> A. y e. ~P ~P A ( ( y =/= (/) /\ [ C.] Or y ) -> |^| y e. y ) ) )
Theorem	ssfin2 8750	A subset of a II-finite set is II-finite. (Contributed by Stefan O'Rear, 2-Nov-2014.) (Revised by Mario Carneiro, 16-May-2015.)
|- ( ( A e. FinII /\ B C_ A ) -> B e. FinII )
Theorem	enfin2i 8751	II-finiteness is a cardinal property. (Contributed by Mario Carneiro, 18-May-2015.)
|- ( A ~~ B -> ( A e. FinII -> B e. FinII ) )
Theorem	fin23lem24 8752	Lemma for fin23 8819. In a class of ordinals, each element is fully identified by those of its predecessors which also belong to the class. (Contributed by Stefan O'Rear, 1-Nov-2014.)
|- ( ( ( Ord A /\ B C_ A ) /\ ( C e. B /\ D e. B ) ) -> ( ( C i^i B ) = ( D i^i B ) <-> C = D ) )
Theorem	fincssdom 8753	In a chain of finite sets, dominance and subset coincide. (Contributed by Stefan O'Rear, 8-Nov-2014.)
|- ( ( A e. Fin /\ B e. Fin /\ ( A C_ B \/ B C_ A ) ) -> ( A ~<_ B <-> A C_ B ) )
Theorem	fin23lem25 8754	Lemma for fin23 8819. In a chain of finite sets, equinumerosity is equivalent to equality. (Contributed by Stefan O'Rear, 1-Nov-2014.)
|- ( ( A e. Fin /\ B e. Fin /\ ( A C_ B \/ B C_ A ) ) -> ( A ~~ B <-> A = B ) )
Theorem	fin23lem26 8755*	Lemma for fin23lem22 8757. (Contributed by Stefan O'Rear, 1-Nov-2014.)
|- ( ( ( S C_ om /\ -. S e. Fin ) /\ i e. om ) -> E. j e. S ( j i^i S ) ~~ i )
Theorem	fin23lem23 8756*	Lemma for fin23lem22 8757. (Contributed by Stefan O'Rear, 1-Nov-2014.)
|- ( ( ( S C_ om /\ -. S e. Fin ) /\ i e. om ) -> E! j e. S ( j i^i S ) ~~ i )
Theorem	fin23lem22 8757*	Lemma for fin23 8819 but could be used elsewhere if we find a good name for it. Explicit construction of a bijection (actually an isomorphism, see fin23lem27 8758) between an infinite subset of om and om itself. (Contributed by Stefan O'Rear, 1-Nov-2014.)
|- C = ( i e. om |-> ( iota_ j e. S ( j i^i S ) ~~ i ) )   =>    |- ( ( S C_ om /\ -. S e. Fin ) -> C : om -1-1-onto-> S )
Theorem	fin23lem27 8758*	The mapping constructed in fin23lem22 8757 is in fact an isomorphism. (Contributed by Stefan O'Rear, 2-Nov-2014.)
|- C = ( i e. om |-> ( iota_ j e. S ( j i^i S ) ~~ i ) )   =>    |- ( ( S C_ om /\ -. S e. Fin ) -> C Isom _E , _E ( om , S ) )
Theorem	isfin3ds 8759*	Property of a III-finite set (descending sequence version). (Contributed by Mario Carneiro, 16-May-2015.)
|- F = { g | A. a e. ( ~P g ^m om ) ( A. b e. om ( a ` suc b ) C_ ( a ` b ) -> |^| ran a e. ran a ) }   =>    |- ( A e. V -> ( A e. F <-> A. f e. ( ~P A ^m om ) ( A. x e. om ( f ` suc x ) C_ ( f ` x ) -> |^| ran f e. ran f ) ) )
Theorem	ssfin3ds 8760*	A subset of a III-finite set is III-finite. (Contributed by Stefan O'Rear, 4-Nov-2014.)
|- F = { g | A. a e. ( ~P g ^m om ) ( A. b e. om ( a ` suc b ) C_ ( a ` b ) -> |^| ran a e. ran a ) }   =>    |- ( ( A e. F /\ B C_ A ) -> B e. F )
Theorem	fin23lem12 8761*	The beginning of the proof that every II-finite set (every chain of subsets has a maximal element) is III-finite (has no denumerable collection of subsets). This first section is dedicated to the construction of U and its intersection. First, the value of U at a successor. (Contributed by Stefan O'Rear, 1-Nov-2014.)
|- U = seq𝜔 ( ( i e. om , u e. _V |-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) , U. ran t )   =>    |- ( A e. om -> ( U ` suc A ) = if ( ( ( t ` A ) i^i ( U ` A ) ) = (/) , ( U ` A ) , ( ( t ` A ) i^i ( U ` A ) ) ) )
Theorem	fin23lem13 8762*	Lemma for fin23 8819. Each step of U is a decrease. (Contributed by Stefan O'Rear, 1-Nov-2014.)
|- U = seq𝜔 ( ( i e. om , u e. _V |-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) , U. ran t )   =>    |- ( A e. om -> ( U ` suc A ) C_ ( U ` A ) )
Theorem	fin23lem14 8763*	Lemma for fin23 8819. U will never evolve to an empty set if it did not start with one. (Contributed by Stefan O'Rear, 1-Nov-2014.)
|- U = seq𝜔 ( ( i e. om , u e. _V |-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) , U. ran t )   =>    |- ( ( A e. om /\ U. ran t =/= (/) ) -> ( U ` A ) =/= (/) )
Theorem	fin23lem15 8764*	Lemma for fin23 8819. U is a monotone function. (Contributed by Stefan O'Rear, 1-Nov-2014.)
|- U = seq𝜔 ( ( i e. om , u e. _V |-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) , U. ran t )   =>    |- ( ( ( A e. om /\ B e. om ) /\ B C_ A ) -> ( U ` A ) C_ ( U ` B ) )
Theorem	fin23lem16 8765*	Lemma for fin23 8819. U ranges over the original set; in particular ran U is a set, although we do not assume here that U is. (Contributed by Stefan O'Rear, 1-Nov-2014.)
|- U = seq𝜔 ( ( i e. om , u e. _V |-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) , U. ran t )   =>    |- U. ran U = U. ran t
Theorem	fin23lem19 8766*	Lemma for fin23 8819. The first set in U to see an input set is either contained in it or disjoint from it. (Contributed by Stefan O'Rear, 1-Nov-2014.)
|- U = seq𝜔 ( ( i e. om , u e. _V |-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) , U. ran t )   =>    |- ( A e. om -> ( ( U ` suc A ) C_ ( t ` A ) \/ ( ( U ` suc A ) i^i ( t ` A ) ) = (/) ) )
Theorem	fin23lem20 8767*	Lemma for fin23 8819. X is either contained in or disjoint from all input sets. (Contributed by Stefan O'Rear, 1-Nov-2014.)
|- U = seq𝜔 ( ( i e. om , u e. _V |-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) , U. ran t )   =>    |- ( A e. om -> ( |^| ran U C_ ( t ` A ) \/ ( |^| ran U i^i ( t ` A ) ) = (/) ) )
Theorem	fin23lem17 8768*	Lemma for fin23 8819. By ? Fin3DS ? , U achieves its minimum ( X in the synopsis above, but we will not be assigning a symbol here). TODO: Fix comment; math symbol Fin3DS does not exist. (Contributed by Stefan O'Rear, 4-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)
|- U = seq𝜔 ( ( i e. om , u e. _V |-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) , U. ran t )   &    |- F = { g | A. a e. ( ~P g ^m om ) ( A. x e. om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) }   =>    |- ( ( U. ran t e. F /\ t : om -1-1-> V ) -> |^| ran U e. ran U )
Theorem	fin23lem21 8769*	Lemma for fin23 8819. X is not empty. We only need here that t has at least one set in its range besides (/); the much stronger hypothesis here will serve as our induction hypothesis though. (Contributed by Stefan O'Rear, 1-Nov-2014.) (Revised by Mario Carneiro, 6-May-2015.)
|- U = seq𝜔 ( ( i e. om , u e. _V |-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) , U. ran t )   &    |- F = { g | A. a e. ( ~P g ^m om ) ( A. x e. om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) }   =>    |- ( ( U. ran t e. F /\ t : om -1-1-> V ) -> |^| ran U =/= (/) )
Theorem	fin23lem28 8770*	Lemma for fin23 8819. The residual is also one-to-one. This preserves the induction invariant. (Contributed by Stefan O'Rear, 2-Nov-2014.)
|- U = seq𝜔 ( ( i e. om , u e. _V |-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) , U. ran t )   &    |- F = { g | A. a e. ( ~P g ^m om ) ( A. x e. om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) }   &    |- P = { v e. om | |^| ran U C_ ( t ` v ) }   &    |- Q = ( w e. om |-> ( iota_ x e. P ( x i^i P ) ~~ w ) )   &    |- R = ( w e. om |-> ( iota_ x e. ( om \ P ) ( x i^i ( om \ P ) ) ~~ w ) )   &    |- Z = if ( P e. Fin , ( t o. R ) , ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) )   =>    |- ( t : om -1-1-> _V -> Z : om -1-1-> _V )
Theorem	fin23lem29 8771*	Lemma for fin23 8819. The residual is built from the same elements as the previous sequence. (Contributed by Stefan O'Rear, 2-Nov-2014.)
|- U = seq𝜔 ( ( i e. om , u e. _V |-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) , U. ran t )   &    |- F = { g | A. a e. ( ~P g ^m om ) ( A. x e. om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) }   &    |- P = { v e. om | |^| ran U C_ ( t ` v ) }   &    |- Q = ( w e. om |-> ( iota_ x e. P ( x i^i P ) ~~ w ) )   &    |- R = ( w e. om |-> ( iota_ x e. ( om \ P ) ( x i^i ( om \ P ) ) ~~ w ) )   &    |- Z = if ( P e. Fin , ( t o. R ) , ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) )   =>    |- U. ran Z C_ U. ran t
Theorem	fin23lem30 8772*	Lemma for fin23 8819. The residual is disjoint from the common set. (Contributed by Stefan O'Rear, 2-Nov-2014.)
|- U = seq𝜔 ( ( i e. om , u e. _V |-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) , U. ran t )   &    |- F = { g | A. a e. ( ~P g ^m om ) ( A. x e. om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) }   &    |- P = { v e. om | |^| ran U C_ ( t ` v ) }   &    |- Q = ( w e. om |-> ( iota_ x e. P ( x i^i P ) ~~ w ) )   &    |- R = ( w e. om |-> ( iota_ x e. ( om \ P ) ( x i^i ( om \ P ) ) ~~ w ) )   &    |- Z = if ( P e. Fin , ( t o. R ) , ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) )   =>    |- ( Fun t -> ( U. ran Z i^i |^| ran U ) = (/) )
Theorem	fin23lem31 8773*	Lemma for fin23 8819. The residual is has a strictly smaller range than the previous sequence. This will be iterated to build an unbounded chain. (Contributed by Stefan O'Rear, 2-Nov-2014.)
|- U = seq𝜔 ( ( i e. om , u e. _V |-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) , U. ran t )   &    |- F = { g | A. a e. ( ~P g ^m om ) ( A. x e. om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) }   &    |- P = { v e. om | |^| ran U C_ ( t ` v ) }   &    |- Q = ( w e. om |-> ( iota_ x e. P ( x i^i P ) ~~ w ) )   &    |- R = ( w e. om |-> ( iota_ x e. ( om \ P ) ( x i^i ( om \ P ) ) ~~ w ) )   &    |- Z = if ( P e. Fin , ( t o. R ) , ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) )   =>    |- ( ( t : om -1-1-> V /\ G e. F /\ U. ran t C_ G ) -> U. ran Z C. U. ran t )
Theorem	fin23lem32 8774*	Lemma for fin23 8819. Wrap the previous construction into a function to hide the hypotheses. (Contributed by Stefan O'Rear, 2-Nov-2014.)
|- U = seq𝜔 ( ( i e. om , u e. _V |-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) , U. ran t )   &    |- F = { g | A. a e. ( ~P g ^m om ) ( A. x e. om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) }   &    |- P = { v e. om | |^| ran U C_ ( t ` v ) }   &    |- Q = ( w e. om |-> ( iota_ x e. P ( x i^i P ) ~~ w ) )   &    |- R = ( w e. om |-> ( iota_ x e. ( om \ P ) ( x i^i ( om \ P ) ) ~~ w ) )   &    |- Z = if ( P e. Fin , ( t o. R ) , ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) )   =>    |- ( G e. F -> E. f A. b ( ( b : om -1-1-> _V /\ U. ran b C_ G ) -> ( ( f ` b ) : om -1-1-> _V /\ U. ran ( f ` b ) C. U. ran b ) ) )
Theorem	fin23lem33 8775*	Lemma for fin23 8819. Discharge hypotheses. (Contributed by Stefan O'Rear, 2-Nov-2014.)
|- F = { g | A. a e. ( ~P g ^m om ) ( A. x e. om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) }   =>    |- ( G e. F -> E. f A. b ( ( b : om -1-1-> _V /\ U. ran b C_ G ) -> ( ( f ` b ) : om -1-1-> _V /\ U. ran ( f ` b ) C. U. ran b ) ) )
Theorem	fin23lem34 8776*	Lemma for fin23 8819. Establish induction invariants on Y which parameterizes our contradictory chain of subsets. In this section, h is the hypothetically assumed family of subsets, g is the ground set, and i is the induction function constructed in the previous section. (Contributed by Stefan O'Rear, 2-Nov-2014.)
|- F = { g | A. a e. ( ~P g ^m om ) ( A. x e. om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) }   &    |- ( ph -> h : om -1-1-> _V )   &    |- ( ph -> U. ran h C_ G )   &    |- ( ph -> A. j ( ( j : om -1-1-> _V /\ U. ran j C_ G ) -> ( ( i ` j ) : om -1-1-> _V /\ U. ran ( i ` j ) C. U. ran j ) ) )   &    |- Y = ( rec ( i , h ) |` om )   =>    |- ( ( ph /\ A e. om ) -> ( ( Y ` A ) : om -1-1-> _V /\ U. ran ( Y ` A ) C_ G ) )
Theorem	fin23lem35 8777*	Lemma for fin23 8819. Strict order property of Y. (Contributed by Stefan O'Rear, 2-Nov-2014.)
|- F = { g | A. a e. ( ~P g ^m om ) ( A. x e. om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) }   &    |- ( ph -> h : om -1-1-> _V )   &    |- ( ph -> U. ran h C_ G )   &    |- ( ph -> A. j ( ( j : om -1-1-> _V /\ U. ran j C_ G ) -> ( ( i ` j ) : om -1-1-> _V /\ U. ran ( i ` j ) C. U. ran j ) ) )   &    |- Y = ( rec ( i , h ) |` om )   =>    |- ( ( ph /\ A e. om ) -> U. ran ( Y ` suc A ) C. U. ran ( Y ` A ) )
Theorem	fin23lem36 8778*	Lemma for fin23 8819. Weak order property of Y. (Contributed by Stefan O'Rear, 2-Nov-2014.)
|- F = { g | A. a e. ( ~P g ^m om ) ( A. x e. om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) }   &    |- ( ph -> h : om -1-1-> _V )   &    |- ( ph -> U. ran h C_ G )   &    |- ( ph -> A. j ( ( j : om -1-1-> _V /\ U. ran j C_ G ) -> ( ( i ` j ) : om -1-1-> _V /\ U. ran ( i ` j ) C. U. ran j ) ) )   &    |- Y = ( rec ( i , h ) |` om )   =>    |- ( ( ( A e. om /\ B e. om ) /\ ( B C_ A /\ ph ) ) -> U. ran ( Y ` A ) C_ U. ran ( Y ` B ) )
Theorem	fin23lem38 8779*	Lemma for fin23 8819. The contradictory chain has no minimum. (Contributed by Stefan O'Rear, 2-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)
|- F = { g | A. a e. ( ~P g ^m om ) ( A. x e. om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) }   &    |- ( ph -> h : om -1-1-> _V )   &    |- ( ph -> U. ran h C_ G )   &    |- ( ph -> A. j ( ( j : om -1-1-> _V /\ U. ran j C_ G ) -> ( ( i ` j ) : om -1-1-> _V /\ U. ran ( i ` j ) C. U. ran j ) ) )   &    |- Y = ( rec ( i , h ) |` om )   =>    |- ( ph -> -. |^| ran ( b e. om |-> U. ran ( Y ` b ) ) e. ran ( b e. om |-> U. ran ( Y ` b ) ) )
Theorem	fin23lem39 8780*	Lemma for fin23 8819. Thus, we have that g could not have been in F after all. (Contributed by Stefan O'Rear, 4-Nov-2014.)
|- F = { g | A. a e. ( ~P g ^m om ) ( A. x e. om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) }   &    |- ( ph -> h : om -1-1-> _V )   &    |- ( ph -> U. ran h C_ G )   &    |- ( ph -> A. j ( ( j : om -1-1-> _V /\ U. ran j C_ G ) -> ( ( i ` j ) : om -1-1-> _V /\ U. ran ( i ` j ) C. U. ran j ) ) )   &    |- Y = ( rec ( i , h ) |` om )   =>    |- ( ph -> -. G e. F )
Theorem	fin23lem40 8781*	Lemma for fin23 8819. FinII sets satisfy the descending chain condition. (Contributed by Stefan O'Rear, 3-Nov-2014.)
|- F = { g | A. a e. ( ~P g ^m om ) ( A. x e. om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) }   =>    |- ( A e. FinII -> A e. F )
Theorem	fin23lem41 8782*	Lemma for fin23 8819. A set which satisfies the descending sequence condition must be III-finite. (Contributed by Stefan O'Rear, 2-Nov-2014.)
|- F = { g | A. a e. ( ~P g ^m om ) ( A. x e. om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) }   =>    |- ( A e. F -> A e. FinIII )
Theorem	isf32lem1 8783*	Lemma for isfin3-2 8797. Derive weak ordering property. (Contributed by Stefan O'Rear, 5-Nov-2014.)
|- ( ph -> F : om --> ~P G )   &    |- ( ph -> A. x e. om ( F ` suc x ) C_ ( F ` x ) )   &    |- ( ph -> -. |^| ran F e. ran F )   =>    |- ( ( ( A e. om /\ B e. om ) /\ ( B C_ A /\ ph ) ) -> ( F ` A ) C_ ( F ` B ) )
Theorem	isf32lem2 8784*	Lemma for isfin3-2 8797. Non-minimum implies that there is always another decrease. (Contributed by Stefan O'Rear, 5-Nov-2014.)
|- ( ph -> F : om --> ~P G )   &    |- ( ph -> A. x e. om ( F ` suc x ) C_ ( F ` x ) )   &    |- ( ph -> -. |^| ran F e. ran F )   =>    |- ( ( ph /\ A e. om ) -> E. a e. om ( A e. a /\ ( F ` suc a ) C. ( F ` a ) ) )
Theorem	isf32lem3 8785*	Lemma for isfin3-2 8797. Being a chain, difference sets are disjoint (one case). (Contributed by Stefan O'Rear, 5-Nov-2014.)
|- ( ph -> F : om --> ~P G )   &    |- ( ph -> A. x e. om ( F ` suc x ) C_ ( F ` x ) )   &    |- ( ph -> -. |^| ran F e. ran F )   =>    |- ( ( ( A e. om /\ B e. om ) /\ ( B e. A /\ ph ) ) -> ( ( ( F ` A ) \ ( F ` suc A ) ) i^i ( ( F ` B ) \ ( F ` suc B ) ) ) = (/) )
Theorem	isf32lem4 8786*	Lemma for isfin3-2 8797. Being a chain, difference sets are disjoint. (Contributed by Stefan O'Rear, 5-Nov-2014.)
|- ( ph -> F : om --> ~P G )   &    |- ( ph -> A. x e. om ( F ` suc x ) C_ ( F ` x ) )   &    |- ( ph -> -. |^| ran F e. ran F )   =>    |- ( ( ( ph /\ A =/= B ) /\ ( A e. om /\ B e. om ) ) -> ( ( ( F ` A ) \ ( F ` suc A ) ) i^i ( ( F ` B ) \ ( F ` suc B ) ) ) = (/) )
Theorem	isf32lem5 8787*	Lemma for isfin3-2 8797. There are infinite decrease points. (Contributed by Stefan O'Rear, 5-Nov-2014.)
|- ( ph -> F : om --> ~P G )   &    |- ( ph -> A. x e. om ( F ` suc x ) C_ ( F ` x ) )   &    |- ( ph -> -. |^| ran F e. ran F )   &    |- S = { y e. om | ( F ` suc y ) C. ( F ` y ) }   =>    |- ( ph -> -. S e. Fin )
Theorem	isf32lem6 8788*	Lemma for isfin3-2 8797. Each K value is nonempty. (Contributed by Stefan O'Rear, 5-Nov-2014.)
|- ( ph -> F : om --> ~P G )   &    |- ( ph -> A. x e. om ( F ` suc x ) C_ ( F ` x ) )   &    |- ( ph -> -. |^| ran F e. ran F )   &    |- S = { y e. om | ( F ` suc y ) C. ( F ` y ) }   &    |- J = ( u e. om |-> ( iota_ v e. S ( v i^i S ) ~~ u ) )   &    |- K = ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) o. J )   =>    |- ( ( ph /\ A e. om ) -> ( K ` A ) =/= (/) )
Theorem	isf32lem7 8789*	Lemma for isfin3-2 8797. Different K values are disjoint. (Contributed by Stefan O'Rear, 5-Nov-2014.)
|- ( ph -> F : om --> ~P G )   &    |- ( ph -> A. x e. om ( F ` suc x ) C_ ( F ` x ) )   &    |- ( ph -> -. |^| ran F e. ran F )   &    |- S = { y e. om | ( F ` suc y ) C. ( F ` y ) }   &    |- J = ( u e. om |-> ( iota_ v e. S ( v i^i S ) ~~ u ) )   &    |- K = ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) o. J )   =>    |- ( ( ( ph /\ A =/= B ) /\ ( A e. om /\ B e. om ) ) -> ( ( K ` A ) i^i ( K ` B ) ) = (/) )
Theorem	isf32lem8 8790*	Lemma for isfin3-2 8797. K sets are subsets of the base. (Contributed by Stefan O'Rear, 6-Nov-2014.)
|- ( ph -> F : om --> ~P G )   &    |- ( ph -> A. x e. om ( F ` suc x ) C_ ( F ` x ) )   &    |- ( ph -> -. |^| ran F e. ran F )   &    |- S = { y e. om | ( F ` suc y ) C. ( F ` y ) }   &    |- J = ( u e. om |-> ( iota_ v e. S ( v i^i S ) ~~ u ) )   &    |- K = ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) o. J )   =>    |- ( ( ph /\ A e. om ) -> ( K ` A ) C_ G )
Theorem	isf32lem9 8791*	Lemma for isfin3-2 8797. Construction of the onto function. (Contributed by Stefan O'Rear, 5-Nov-2014.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- ( ph -> F : om --> ~P G )   &    |- ( ph -> A. x e. om ( F ` suc x ) C_ ( F ` x ) )   &    |- ( ph -> -. |^| ran F e. ran F )   &    |- S = { y e. om | ( F ` suc y ) C. ( F ` y ) }   &    |- J = ( u e. om |-> ( iota_ v e. S ( v i^i S ) ~~ u ) )   &    |- K = ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) o. J )   &    |- L = ( t e. G |-> ( iota s ( s e. om /\ t e. ( K ` s ) ) ) )   =>    |- ( ph -> L : G -onto-> om )
Theorem	isf32lem10 8792*	Lemma for isfin3-2 . Write in terms of weak dominance. (Contributed by Stefan O'Rear, 6-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)
|- ( ph -> F : om --> ~P G )   &    |- ( ph -> A. x e. om ( F ` suc x ) C_ ( F ` x ) )   &    |- ( ph -> -. |^| ran F e. ran F )   &    |- S = { y e. om | ( F ` suc y ) C. ( F ` y ) }   &    |- J = ( u e. om |-> ( iota_ v e. S ( v i^i S ) ~~ u ) )   &    |- K = ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) o. J )   &    |- L = ( t e. G |-> ( iota s ( s e. om /\ t e. ( K ` s ) ) ) )   =>    |- ( ph -> ( G e. V -> om ~<_* G ) )
Theorem	isf32lem11 8793*	Lemma for isfin3-2 8797. Remove hypotheses from isf32lem10 8792. (Contributed by Stefan O'Rear, 17-May-2015.)
|- ( ( G e. V /\ ( F : om --> ~P G /\ A. b e. om ( F ` suc b ) C_ ( F ` b ) /\ -. |^| ran F e. ran F ) ) -> om ~<_* G )
Theorem	isf32lem12 8794*	Lemma for isfin3-2 8797. (Contributed by Stefan O'Rear, 6-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)
|- F = { g | A. a e. ( ~P g ^m om ) ( A. x e. om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) }   =>    |- ( G e. V -> ( -. om ~<_* G -> G e. F ) )
Theorem	isfin32i 8795	One half of isfin3-2 8797. (Contributed by Mario Carneiro, 3-Jun-2015.)
|- ( A e. FinIII -> -. om ~<_* A )
Theorem	isf33lem 8796*	Lemma for isfin3-3 8798. (Contributed by Stefan O'Rear, 17-May-2015.)
|- FinIII = { g | A. a e. ( ~P g ^m om ) ( A. x e. om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) }
Theorem	isfin3-2 8797	Weakly Dedekind-infinite sets are exactly those which can be mapped onto om. (Contributed by Stefan O'Rear, 6-Nov-2014.) (Proof shortened by Mario Carneiro, 17-May-2015.)
|- ( A e. V -> ( A e. FinIII <-> -. om ~<_* A ) )
Theorem	isfin3-3 8798*	Weakly Dedekind-infinite sets are exactly those with an om-indexed descending chain of subsets. (Contributed by Stefan O'Rear, 7-Nov-2014.)
|- ( A e. V -> ( A e. FinIII <-> A. f e. ( ~P A ^m om ) ( A. x e. om ( f ` suc x ) C_ ( f ` x ) -> |^| ran f e. ran f ) ) )
Theorem	fin33i 8799*	Inference from isfin3-3 8798. (This is actually a bit stronger than isfin3-3 8798 because it does not assume F is a set and does not use the Axiom of Infinity either.) (Contributed by Mario Carneiro, 17-May-2015.)
|- ( ( A e. FinIII /\ F : om --> ~P A /\ A. x e. om ( F ` suc x ) C_ ( F ` x ) ) -> |^| ran F e. ran F )
Theorem	compsscnvlem 8800*	Lemma for compsscnv 8801. (Contributed by Mario Carneiro, 17-May-2015.)
|- ( ( x e. ~P A /\ y = ( A \ x ) ) -> ( y e. ~P A /\ x = ( A \ y ) ) )