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
Syntax	cfin5 8701	Extend class notation to include the class of V-finite sets.
class FinV
Syntax	cfin6 8702	Extend class notation to include the class of VI-finite sets.
class FinVI
Syntax	cfin7 8703	Extend class notation to include the class of VII-finite sets.
class FinVII
Definition	df-fin1a 8704*	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 7572 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 8705*	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 8706*	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 8707	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 8708	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 8709	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 8710*	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 8711*	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 8712	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 8713*	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 8714	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 8715	Definition of a III-finite set. (Contributed by Stefan O'Rear, 16-May-2015.)
|- ( A e. FinIII <-> ~P A e. FinIV )
Theorem	isfin4 8716*	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 8717	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 8718	Definition of a V-finite set. (Contributed by Stefan O'Rear, 16-May-2015.)
|- ( A e. FinV <-> ( A = (/) \/ A ~< ( A +c A ) ) )
Theorem	isfin6 8719	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 8720*	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 8721	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 8722	Lemma for infpssr 8727. (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 8723	Lemma for infpssr 8727. (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 8724	Lemma for infpssr 8727. (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 8725	Lemma for infpssr 8727. (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 8726	Lemma for infpssr 8727. (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 8727	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 8728	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 8729	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 8730	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 8731	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 8732*	Alternate proof of infpss 8636, shorter but requiring Replacement (ax-rep 4529). (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 8733	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 8734	Alternate definition of IV-finite sets: they are strictly dominated by their successors. (Thus, the proper subset referred to in isfin4 8716 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 8735*	Lemma for isfin2-2 8738. 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 8736*	Lemma for isfin2-2 8738. (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 8737	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 8738*	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 8739	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 8740	II-finiteness is a cardinal property. (Contributed by Mario Carneiro, 18-May-2015.)
|- ( A ~~ B -> ( A e. FinII -> B e. FinII ) )
Theorem	fin23lem24 8741	Lemma for fin23 8808. 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 8742	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 8743	Lemma for fin23 8808. 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 8744*	Lemma for fin23lem22 8746. (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 8745*	Lemma for fin23lem22 8746. (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 8746*	Lemma for fin23 8808 but could be used elsewhere if we find a good name for it. Explicit construction of a bijection (actually an isomorphism, see fin23lem27 8747) 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 8747*	The mapping constructed in fin23lem22 8746 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 8748*	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 8749*	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 8750*	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 8751*	Lemma for fin23 8808. 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 8752*	Lemma for fin23 8808. 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 8753*	Lemma for fin23 8808. 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 8754*	Lemma for fin23 8808. 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 8755*	Lemma for fin23 8808. 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 8756*	Lemma for fin23 8808. 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 8757*	Lemma for fin23 8808. 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 8758*	Lemma for fin23 8808. 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 8759*	Lemma for fin23 8808. 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 8760*	Lemma for fin23 8808. 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 8761*	Lemma for fin23 8808. 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 8762*	Lemma for fin23 8808. 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 8763*	Lemma for fin23 8808. 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 8764*	Lemma for fin23 8808. 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 8765*	Lemma for fin23 8808. 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 8766*	Lemma for fin23 8808. 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 8767*	Lemma for fin23 8808. 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 8768*	Lemma for fin23 8808. 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 8769*	Lemma for fin23 8808. 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 8770*	Lemma for fin23 8808. 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 8771*	Lemma for fin23 8808. 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 8772*	Lemma for isfin3-2 8786. 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 8773*	Lemma for isfin3-2 8786. 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 8774*	Lemma for isfin3-2 8786. 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 8775*	Lemma for isfin3-2 8786. 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 8776*	Lemma for isfin3-2 8786. 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 8777*	Lemma for isfin3-2 8786. 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 8778*	Lemma for isfin3-2 8786. 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 8779*	Lemma for isfin3-2 8786. 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 8780*	Lemma for isfin3-2 8786. 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 8781*	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 8782*	Lemma for isfin3-2 8786. Remove hypotheses from isf32lem10 8781. (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 8783*	Lemma for isfin3-2 8786. (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 8784	One half of isfin3-2 8786. (Contributed by Mario Carneiro, 3-Jun-2015.)
|- ( A e. FinIII -> -. om ~<_* A )
Theorem	isf33lem 8785*	Lemma for isfin3-3 8787. (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 8786	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 8787*	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 8788*	Inference from isfin3-3 8787. (This is actually a bit stronger than isfin3-3 8787 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 8789*	Lemma for compsscnv 8790. (Contributed by Mario Carneiro, 17-May-2015.)
|- ( ( x e. ~P A /\ y = ( A \ x ) ) -> ( y e. ~P A /\ x = ( A \ y ) ) )
Theorem	compsscnv 8790*	Complementation on a power set lattice is an involution. (Contributed by Mario Carneiro, 17-May-2015.)
|- F = ( x e. ~P A |-> ( A \ x ) )   =>    |- `' F = F
Theorem	isf34lem1 8791*	Lemma for isfin3-4 8801. (Contributed by Stefan O'Rear, 7-Nov-2014.)
|- F = ( x e. ~P A |-> ( A \ x ) )   =>    |- ( ( A e. V /\ X C_ A ) -> ( F ` X ) = ( A \ X ) )
Theorem	isf34lem2 8792*	Lemma for isfin3-4 8801. (Contributed by Stefan O'Rear, 7-Nov-2014.)
|- F = ( x e. ~P A |-> ( A \ x ) )   =>    |- ( A e. V -> F : ~P A --> ~P A )
Theorem	compssiso 8793*	Complementation is an antiautomorphism on power set lattices. (Contributed by Stefan O'Rear, 4-Nov-2014.) (Proof shortened by Mario Carneiro, 17-May-2015.)
|- F = ( x e. ~P A |-> ( A \ x ) )   =>    |- ( A e. V -> F Isom [ C.] , `' [ C.] ( ~P A , ~P A ) )
Theorem	isf34lem3 8794*	Lemma for isfin3-4 8801. (Contributed by Stefan O'Rear, 7-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)
|- F = ( x e. ~P A |-> ( A \ x ) )   =>    |- ( ( A e. V /\ X C_ ~P A ) -> ( F " ( F " X ) ) = X )
Theorem	compss 8795*	Express image under of the complementation isomorphism. (Contributed by Stefan O'Rear, 5-Nov-2014.) (Proof shortened by Mario Carneiro, 17-May-2015.)
|- F = ( x e. ~P A |-> ( A \ x ) )   =>    |- ( F " G ) = { y e. ~P A | ( A \ y ) e. G }
Theorem	isf34lem4 8796*	Lemma for isfin3-4 8801. (Contributed by Stefan O'Rear, 7-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)
|- F = ( x e. ~P A |-> ( A \ x ) )   =>    |- ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( F ` U. X ) = |^| ( F " X ) )
Theorem	isf34lem5 8797*	Lemma for isfin3-4 8801. (Contributed by Stefan O'Rear, 7-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)
|- F = ( x e. ~P A |-> ( A \ x ) )   =>    |- ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( F ` |^| X ) = U. ( F " X ) )
Theorem	isf34lem7 8798*	Lemma for isfin3-4 8801. (Contributed by Stefan O'Rear, 7-Nov-2014.)
|- F = ( x e. ~P A |-> ( A \ x ) )   =>    |- ( ( A e. FinIII /\ G : om --> ~P A /\ A. y e. om ( G ` y ) C_ ( G ` suc y ) ) -> U. ran G e. ran G )
Theorem	isf34lem6 8799*	Lemma for isfin3-4 8801. (Contributed by Stefan O'Rear, 7-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)
|- F = ( x e. ~P A |-> ( A \ x ) )   =>    |- ( A e. V -> ( A e. FinIII <-> A. f e. ( ~P A ^m om ) ( A. y e. om ( f ` y ) C_ ( f ` suc y ) -> U. ran f e. ran f ) ) )
Theorem	fin34i 8800*	Inference from isfin3-4 8801. (Contributed by Mario Carneiro, 17-May-2015.)
|- ( ( A e. FinIII /\ G : om --> ~P A /\ A. x e. om ( G ` x ) C_ ( G ` suc x ) ) -> U. ran G e. ran G )