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	ssfin3ds 8701*	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 8702*	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 8703*	Lemma for fin23 8760. 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 8704*	Lemma for fin23 8760. 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 8705*	Lemma for fin23 8760. 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 8706*	Lemma for fin23 8760. 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 8707*	Lemma for fin23 8760. 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 8708*	Lemma for fin23 8760. 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 8709*	Lemma for fin23 8760. 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 8710*	Lemma for fin23 8760. 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 8711*	Lemma for fin23 8760. 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 8712*	Lemma for fin23 8760. 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 8713*	Lemma for fin23 8760. 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 8714*	Lemma for fin23 8760. 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 8715*	Lemma for fin23 8760. 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 8716*	Lemma for fin23 8760. 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 8717*	Lemma for fin23 8760. 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 8718*	Lemma for fin23 8760. 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 8719*	Lemma for fin23 8760. 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 8720*	Lemma for fin23 8760. 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 8721*	Lemma for fin23 8760. 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 8722*	Lemma for fin23 8760. 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 8723*	Lemma for fin23 8760. 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 8724*	Lemma for isfin3-2 8738. 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 8725*	Lemma for isfin3-2 8738. 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 8726*	Lemma for isfin3-2 8738. 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 8727*	Lemma for isfin3-2 8738. 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 8728*	Lemma for isfin3-2 8738. 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 8729*	Lemma for isfin3-2 8738. 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 8730*	Lemma for isfin3-2 8738. 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 8731*	Lemma for isfin3-2 8738. 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 8732*	Lemma for isfin3-2 8738. 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 8733*	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 8734*	Lemma for isfin3-2 8738. Remove hypotheses from isf32lem10 8733. (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 8735*	Lemma for isfin3-2 8738. (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 8736	One half of isfin3-2 8738. (Contributed by Mario Carneiro, 3-Jun-2015.)
|- ( A e. FinIII -> -. om ~<_* A )
Theorem	isf33lem 8737*	Lemma for isfin3-3 8739. (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 8738	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 8739*	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 8740*	Inference from isfin3-3 8739. (This is actually a bit stronger than isfin3-3 8739 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 8741*	Lemma for compsscnv 8742. (Contributed by Mario Carneiro, 17-May-2015.)
|- ( ( x e. ~P A /\ y = ( A \ x ) ) -> ( y e. ~P A /\ x = ( A \ y ) ) )
Theorem	compsscnv 8742*	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 8743*	Lemma for isfin3-4 8753. (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 8744*	Lemma for isfin3-4 8753. (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 8745*	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 8746*	Lemma for isfin3-4 8753. (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 8747*	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 8748*	Lemma for isfin3-4 8753. (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 8749*	Lemma for isfin3-4 8753. (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 8750*	Lemma for isfin3-4 8753. (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 8751*	Lemma for isfin3-4 8753. (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 8752*	Inference from isfin3-4 8753. (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 )
Theorem	isfin3-4 8753*	Weakly Dedekind-infinite sets are exactly those with an om-indexed ascending chain of subsets. (Contributed by Stefan O'Rear, 7-Nov-2014.) (Proof shortened by Mario Carneiro, 17-May-2015.)
|- ( A e. V -> ( A e. FinIII <-> A. f e. ( ~P A ^m om ) ( A. x e. om ( f ` x ) C_ ( f ` suc x ) -> U. ran f e. ran f ) ) )
Theorem	fin11a 8754	Every I-finite set is Ia-finite. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Revised by Mario Carneiro, 17-May-2015.)
|- ( A e. Fin -> A e. FinIa )
Theorem	enfin1ai 8755	Ia-finiteness is a cardinal property. (Contributed by Mario Carneiro, 18-May-2015.)
|- ( A ~~ B -> ( A e. FinIa -> B e. FinIa ) )
Theorem	isfin1-2 8756	A set is finite in the usual sense iff the power set of its power set is Dedekind finite. (Contributed by Stefan O'Rear, 3-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)
|- ( A e. Fin <-> ~P ~P A e. FinIV )
Theorem	isfin1-3 8757	A set is I-finite iff every system of subsets contains a maximal subset. Definition I of [Levy58] p. 2. (Contributed by Stefan O'Rear, 4-Nov-2014.) (Proof shortened by Mario Carneiro, 17-May-2015.)
|- ( A e. V -> ( A e. Fin <-> `' [ C.] Fr ~P A ) )
Theorem	isfin1-4 8758	A set is I-finite iff every system of subsets contains a minimal subset. (Contributed by Stefan O'Rear, 4-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)
|- ( A e. V -> ( A e. Fin <-> [ C.] Fr ~P A ) )
Theorem	dffin1-5 8759	Compact quantifier-free version of the standard definition df-fin 7513. (Contributed by Stefan O'Rear, 6-Jan-2015.)
|- Fin = ( ~~ " om )
Theorem	fin23 8760	Every II-finite set (every chain of subsets has a maximal element) is III-finite (has no denumerable collection of subsets). The proof here is the only one I could find, from http://matwbn.icm.edu.pl/ksiazki/fm/fm6/fm619.pdf p.94 (writeup by Tarski, credited to Kuratowski). Translated into English and modern notation, the proof proceeds as follows (variables renamed for uniqueness): Suppose for a contradiction that A is a set which is II-finite but not III-finite. For any countable sequence of distinct subsets T of A, we can form a decreasing sequence of nonempty subsets ( U ` T ) by taking finite intersections of initial segments of T while skipping over any element of T which would cause the intersection to be empty. By II-finiteness (as fin2i2 8689) this sequence contains its intersection, call it Y; since by induction every subset in the sequence U is nonempty, the intersection must be nonempty. Suppose that an element X of T has nonempty intersection with Y. Thus, said element has a nonempty intersection with the corresponding element of U, therefore it was used in the construction of U and all further elements of U are subsets of X, thus X contains the Y. That is, all elements of X either contain Y or are disjoint from it. Since there are only two cases, there must exist an infinite subset of T which uniformly either contain Y or are disjoint from it. In the former case we can create an infinite set by subtracting Y from each element. In either case, call the result Z; this is an infinite set of subsets of A, each of which is disjoint from Y and contained in the union of T; the union of Z is strictly contained in the union of T, because only the latter is a superset of the nonempty set Y. The preceding four steps may be iterated a countable number of times starting from the assumed denumerable set of subsets to produce a denumerable sequence B of the T sets from each stage. Great caution is required to avoid ax-dc 8817 here; in particular an effective version of the pigeonhole principle (for aleph-null pigeons and 2 holes) is required. Since a denumerable set of subsets is assumed to exist, we can conclude om e. _V without the axiom. This B sequence is strictly decreasing, thus it has no minimum, contradicting the first assumption. (Contributed by Stefan O'Rear, 2-Nov-2014.) (Proof shortened by Mario Carneiro, 17-May-2015.)
|- ( A e. FinII -> A e. FinIII )
Theorem	fin34 8761	Every III-finite set is IV-finite. (Contributed by Stefan O'Rear, 30-Oct-2014.)
|- ( A e. FinIII -> A e. FinIV )
Theorem	isfin5-2 8762	Alternate definition of V-finite which emphasizes the idempotent behavior of V-infinite sets. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Revised by Mario Carneiro, 17-May-2015.)
|- ( A e. V -> ( A e. FinV <-> -. ( A =/= (/) /\ A ~~ ( A +c A ) ) ) )
Theorem	fin45 8763	Every IV-finite set is V-finite: if we can pack two copies of the set into itself, we can certainly leave space. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Proof shortened by Mario Carneiro, 18-May-2015.)
|- ( A e. FinIV -> A e. FinV )
Theorem	fin56 8764	Every V-finite set is VI-finite because multiplication dominates addition for cardinals. (Contributed by Stefan O'Rear, 29-Oct-2014.) (Revised by Mario Carneiro, 17-May-2015.)
|- ( A e. FinV -> A e. FinVI )
Theorem	fin17 8765	Every I-finite set is VII-finite. (Contributed by Mario Carneiro, 17-May-2015.)
|- ( A e. Fin -> A e. FinVII )
Theorem	fin67 8766	Every VI-finite set is VII-finite. (Contributed by Stefan O'Rear, 29-Oct-2014.) (Revised by Mario Carneiro, 17-May-2015.)
|- ( A e. FinVI -> A e. FinVII )
Theorem	isfin7-2 8767	A set is VII-finite iff it is non-well-orderable or finite. (Contributed by Mario Carneiro, 17-May-2015.)
|- ( A e. V -> ( A e. FinVII <-> ( A e. dom card -> A e. Fin ) ) )
Theorem	fin71num 8768	A well-orderable set is VII-finite iff it is I-finite. Thus, even without choice, on the class of well-orderable sets all eight definitions of finite set coincide. (Contributed by Mario Carneiro, 18-May-2015.)
|- ( A e. dom card -> ( A e. FinVII <-> A e. Fin ) )
Theorem	dffin7-2 8769	Class form of isfin7-2 8767. (Contributed by Mario Carneiro, 17-May-2015.)
|- FinVII = ( Fin u. ( _V \ dom card ) )
Theorem	dfacfin7 8770	Axiom of Choice equivalent: the VII-finite sets are the same as I-finite sets. (Contributed by Mario Carneiro, 18-May-2015.)
|- (CHOICE <-> FinVII = Fin )
Theorem	fin1a2lem1 8771	Lemma for fin1a2 8786. (Contributed by Stefan O'Rear, 7-Nov-2014.)
|- S = ( x e. On |-> suc x )   =>    |- ( A e. On -> ( S ` A ) = suc A )
Theorem	fin1a2lem2 8772	Lemma for fin1a2 8786. (Contributed by Stefan O'Rear, 7-Nov-2014.)
|- S = ( x e. On |-> suc x )   =>    |- S : On -1-1-> On
Theorem	fin1a2lem3 8773	Lemma for fin1a2 8786. (Contributed by Stefan O'Rear, 7-Nov-2014.)
|- E = ( x e. om |-> ( 2o .o x ) )   =>    |- ( A e. om -> ( E ` A ) = ( 2o .o A ) )
Theorem	fin1a2lem4 8774	Lemma for fin1a2 8786. (Contributed by Stefan O'Rear, 7-Nov-2014.)
|- E = ( x e. om |-> ( 2o .o x ) )   =>    |- E : om -1-1-> om
Theorem	fin1a2lem5 8775	Lemma for fin1a2 8786. (Contributed by Stefan O'Rear, 7-Nov-2014.)
|- E = ( x e. om |-> ( 2o .o x ) )   =>    |- ( A e. om -> ( A e. ran E <-> -. suc A e. ran E ) )
Theorem	fin1a2lem6 8776	Lemma for fin1a2 8786. Establish that om can be broken into two equipollent pieces. (Contributed by Stefan O'Rear, 7-Nov-2014.)
|- E = ( x e. om |-> ( 2o .o x ) )   &    |- S = ( x e. On |-> suc x )   =>    |- ( S |` ran E ) : ran E -1-1-onto-> ( om \ ran E )
Theorem	fin1a2lem7 8777*	Lemma for fin1a2 8786. Split a III-infinite set in two pieces. (Contributed by Stefan O'Rear, 7-Nov-2014.)
|- E = ( x e. om |-> ( 2o .o x ) )   &    |- S = ( x e. On |-> suc x )   =>    |- ( ( A e. V /\ A. y e. ~P A ( y e. FinIII \/ ( A \ y ) e. FinIII ) ) -> A e. FinIII )
Theorem	fin1a2lem8 8778*	Lemma for fin1a2 8786. Split a III-infinite set in two pieces. (Contributed by Stefan O'Rear, 7-Nov-2014.)
|- ( ( A e. V /\ A. x e. ~P A ( x e. FinIII \/ ( A \ x ) e. FinIII ) ) -> A e. FinIII )
Theorem	fin1a2lem9 8779*	Lemma for fin1a2 8786. In a chain of finite sets, initial segments are finite. (Contributed by Stefan O'Rear, 8-Nov-2014.)
|- ( ( [ C.] Or X /\ X C_ Fin /\ A e. om ) -> { b e. X | b ~<_ A } e. Fin )
Theorem	fin1a2lem10 8780	Lemma for fin1a2 8786. A nonempty finite union of members of a chain is a member of the chain. (Contributed by Stefan O'Rear, 8-Nov-2014.)
|- ( ( A =/= (/) /\ A e. Fin /\ [ C.] Or A ) -> U. A e. A )
Theorem	fin1a2lem11 8781*	Lemma for fin1a2 8786. (Contributed by Stefan O'Rear, 8-Nov-2014.)
|- ( ( [ C.] Or A /\ A C_ Fin ) -> ran ( b e. om |-> U. { c e. A | c ~<_ b } ) = ( A u. { (/) } ) )
Theorem	fin1a2lem12 8782	Lemma for fin1a2 8786. (Contributed by Stefan O'Rear, 8-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)
|- ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( A C_ Fin /\ A =/= (/) ) ) -> -. B e. FinIII )
Theorem	fin1a2lem13 8783	Lemma for fin1a2 8786. (Contributed by Stefan O'Rear, 8-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)
|- ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) -> -. ( B \ C ) e. FinII )
Theorem	fin12 8784	Weak theorem which skips Ia but has a trivial proof, needed to prove fin1a2 8786. (Contributed by Stefan O'Rear, 8-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)
|- ( A e. Fin -> A e. FinII )
Theorem	fin1a2s 8785*	An II-infinite set can have an I-infinite part broken off and remain II-infinite. (Contributed by Stefan O'Rear, 8-Nov-2014.) (Proof shortened by Mario Carneiro, 17-May-2015.)
|- ( ( A e. V /\ A. x e. ~P A ( x e. Fin \/ ( A \ x ) e. FinII ) ) -> A e. FinII )
Theorem	fin1a2 8786	Every Ia-finite set is II-finite. Theorem 1 of [Levy58], p. 3. (Contributed by Stefan O'Rear, 8-Nov-2014.) (Proof shortened by Mario Carneiro, 17-May-2015.)
|- ( A e. FinIa -> A e. FinII )
2.6.13  Hereditarily size-limited sets without Choice
Theorem	itunifval 8787*	Function value of iterated unions. EDITORIAL: The iterated unions and order types of ordered sets are split out here because they could conceivably be independently useful. (Contributed by Stefan O'Rear, 11-Feb-2015.)
|- U = ( x e. _V |-> ( rec ( ( y e. _V |-> U. y ) , x ) |` om ) )   =>    |- ( A e. V -> ( U ` A ) = ( rec ( ( y e. _V |-> U. y ) , A ) |` om ) )
Theorem	itunifn 8788*	Functionality of the iterated union. (Contributed by Stefan O'Rear, 11-Feb-2015.)
|- U = ( x e. _V |-> ( rec ( ( y e. _V |-> U. y ) , x ) |` om ) )   =>    |- ( A e. V -> ( U ` A ) Fn om )
Theorem	ituni0 8789*	A zero-fold iterated union. (Contributed by Stefan O'Rear, 11-Feb-2015.)
|- U = ( x e. _V |-> ( rec ( ( y e. _V |-> U. y ) , x ) |` om ) )   =>    |- ( A e. V -> ( ( U ` A ) ` (/) ) = A )
Theorem	itunisuc 8790*	Successor iterated union. (Contributed by Stefan O'Rear, 11-Feb-2015.)
|- U = ( x e. _V |-> ( rec ( ( y e. _V |-> U. y ) , x ) |` om ) )   =>    |- ( ( U ` A ) ` suc B ) = U. ( ( U ` A ) ` B )
Theorem	itunitc1 8791*	Each union iterate is a member of the transitive closure. (Contributed by Stefan O'Rear, 11-Feb-2015.)
|- U = ( x e. _V |-> ( rec ( ( y e. _V |-> U. y ) , x ) |` om ) )   =>    |- ( ( U ` A ) ` B ) C_ ( TC ` A )
Theorem	itunitc 8792*	The union of all union iterates creates the transitive closure; compare trcl 8150. (Contributed by Stefan O'Rear, 11-Feb-2015.)
|- U = ( x e. _V |-> ( rec ( ( y e. _V |-> U. y ) , x ) |` om ) )   =>    |- ( TC ` A ) = U. ran ( U ` A )
Theorem	ituniiun 8793*	Unwrap an iterated union from the "other end". (Contributed by Stefan O'Rear, 11-Feb-2015.)
|- U = ( x e. _V |-> ( rec ( ( y e. _V |-> U. y ) , x ) |` om ) )   =>    |- ( A e. V -> ( ( U ` A ) ` suc B ) = U_ a e. A ( ( U ` a ) ` B ) )
Theorem	hsmexlem7 8794*	Lemma for hsmex 8803. Properties of the recurrent sequence of ordinals. (Contributed by Stefan O'Rear, 14-Feb-2015.)
|- H = ( rec ( ( z e. _V |-> (har ` ~P ( X X. z ) ) ) , (har ` ~P X ) ) |` om )   =>    |- ( H ` (/) ) = (har ` ~P X )
Theorem	hsmexlem8 8795*	Lemma for hsmex 8803. Properties of the recurrent sequence of ordinals. (Contributed by Stefan O'Rear, 14-Feb-2015.)
|- H = ( rec ( ( z e. _V |-> (har ` ~P ( X X. z ) ) ) , (har ` ~P X ) ) |` om )   =>    |- ( a e. om -> ( H ` suc a ) = (har ` ~P ( X X. ( H ` a ) ) ) )
Theorem	hsmexlem9 8796*	Lemma for hsmex 8803. Properties of the recurrent sequence of ordinals. (Contributed by Stefan O'Rear, 14-Feb-2015.)
|- H = ( rec ( ( z e. _V |-> (har ` ~P ( X X. z ) ) ) , (har ` ~P X ) ) |` om )   =>    |- ( a e. om -> ( H ` a ) e. On )
Theorem	hsmexlem1 8797	Lemma for hsmex 8803. Bound the order type of a limited-cardinality set of ordinals. (Contributed by Stefan O'Rear, 14-Feb-2015.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- O = OrdIso ( _E , A )   =>    |- ( ( A C_ On /\ A ~<_* B ) -> dom O e. (har ` ~P B ) )
Theorem	hsmexlem2 8798*	Lemma for hsmex 8803. Bound the order type of a union of sets of ordinals, each of limited order type. Vaguely reminiscent of unictb 8941 but use of order types allows to canonically choose the sub-bijections, removing the choice requirement. (Contributed by Stefan O'Rear, 14-Feb-2015.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- F = OrdIso ( _E , B )   &    |- G = OrdIso ( _E , U_ a e. A B )   =>    |- ( ( A e. _V /\ C e. On /\ A. a e. A ( B e. ~P On /\ dom F e. C ) ) -> dom G e. (har ` ~P ( A X. C ) ) )
Theorem	hsmexlem3 8799*	Lemma for hsmex 8803. Clear I hypothesis and extend previous result by dominance. Note that this could be substantially strengthened, e.g. using the weak Hartogs function, but all we need here is that there be *some* dominating ordinal. (Contributed by Stefan O'Rear, 14-Feb-2015.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- F = OrdIso ( _E , B )   &    |- G = OrdIso ( _E , U_ a e. A B )   =>    |- ( ( ( A ~<_* D /\ C e. On ) /\ A. a e. A ( B e. ~P On /\ dom F e. C ) ) -> dom G e. (har ` ~P ( D X. C ) ) )
Theorem	hsmexlem4 8800*	Lemma for hsmex 8803. The core induction, establishing bounds on the order types of iterated unions of the initial set. (Contributed by Stefan O'Rear, 14-Feb-2015.)
|- X e. _V   &    |- H = ( rec ( ( z e. _V |-> (har ` ~P ( X X. z ) ) ) , (har ` ~P X ) ) |` om )   &    |- U = ( x e. _V |-> ( rec ( ( y e. _V |-> U. y ) , x ) |` om ) )   &    |- S = { a e. U. ( R1 " On ) | A. b e. ( TC ` { a } ) b ~<_ X }   &    |- O = OrdIso ( _E , ( rank " ( ( U ` d ) ` c ) ) )   =>    |- ( ( c e. om /\ d e. S ) -> dom O e. ( H ` c ) )