P. 92 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 9101-9200   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	cfin2 9101	Extend class notation to include the class of II-finite sets.
class FinII
Syntax	cfin4 9102	Extend class notation to include the class of IV-finite sets.
class FinIV
Syntax	cfin3 9103	Extend class notation to include the class of III-finite sets.
class FinIII
Syntax	cfin5 9104	Extend class notation to include the class of V-finite sets.
class FinV
Syntax	cfin6 9105	Extend class notation to include the class of VI-finite sets.
class FinVI
Syntax	cfin7 9106	Extend class notation to include the class of VII-finite sets.
class FinVII
Definition	df-fin1a 9107*	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 7959 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 9108*	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 9109*	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 9110	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 9111	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 9112	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 9113*	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 9114*	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 9115	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 9116*	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 9117	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 9118	Definition of a III-finite set. (Contributed by Stefan O'Rear, 16-May-2015.)
|- ( A e. FinIII <-> ~P A e. FinIV )
Theorem	isfin4 9119*	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 9120	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 9121	Definition of a V-finite set. (Contributed by Stefan O'Rear, 16-May-2015.)
|- ( A e. FinV <-> ( A = (/) \/ A ~< ( A +c A ) ) )
Theorem	isfin6 9122	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 9123*	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 9124	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 9125	Lemma for infpssr 9130. (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 9126	Lemma for infpssr 9130. (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 9127	Lemma for infpssr 9130. (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 9128	Lemma for infpssr 9130. (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 9129	Lemma for infpssr 9130. (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 9130	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 9131	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 9132	Dedekind finite sets have Dedekind finite subsets. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Revised by Mario Carneiro, 6-May-2015.) (Revised by Mario Carneiro, 16-May-2015.)
|- ( ( A e. FinIV /\ B C_ A ) -> B e. FinIV )
Theorem	domfin4 9133	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 9134	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 9135*	Alternate proof of infpss 9039, shorter but requiring Replacement (ax-rep 4771). (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 9136	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 9137	Alternate definition of IV-finite sets: they are strictly dominated by their successors. (Thus, the proper subset referred to in isfin4 9119 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 9138*	Lemma for isfin2-2 9141. 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 9139*	Lemma for isfin2-2 9141. (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 9140	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 9141*	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 9142	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 9143	II-finiteness is a cardinal property. (Contributed by Mario Carneiro, 18-May-2015.)
|- ( A ~~ B -> ( A e. FinII -> B e. FinII ) )
Theorem	fin23lem24 9144	Lemma for fin23 9211. 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 9145	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 9146	Lemma for fin23 9211. 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 9147*	Lemma for fin23lem22 9149. (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 9148*	Lemma for fin23lem22 9149. (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 9149*	Lemma for fin23 9211 but could be used elsewhere if we find a good name for it. Explicit construction of a bijection (actually an isomorphism, see fin23lem27 9150) 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 9150*	The mapping constructed in fin23lem22 9149 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 9151*	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 9152*	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 9153*	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 9154*	Lemma for fin23 9211. 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 9155*	Lemma for fin23 9211. 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 9156*	Lemma for fin23 9211. 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 9157*	Lemma for fin23 9211. 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 9158*	Lemma for fin23 9211. 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 9159*	Lemma for fin23 9211. 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 9160*	Lemma for fin23 9211. 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 9161*	Lemma for fin23 9211. 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 9162*	Lemma for fin23 9211. 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 9163*	Lemma for fin23 9211. 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 9164*	Lemma for fin23 9211. 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 9165*	Lemma for fin23 9211. 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 9166*	Lemma for fin23 9211. 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 9167*	Lemma for fin23 9211. 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 9168*	Lemma for fin23 9211. 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 9169*	Lemma for fin23 9211. 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 9170*	Lemma for fin23 9211. 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 9171*	Lemma for fin23 9211. 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 9172*	Lemma for fin23 9211. 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 9173*	Lemma for fin23 9211. 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 9174*	Lemma for fin23 9211. 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 9175*	Lemma for isfin3-2 9189. 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 9176*	Lemma for isfin3-2 9189. 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 9177*	Lemma for isfin3-2 9189. 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 9178*	Lemma for isfin3-2 9189. 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 9179*	Lemma for isfin3-2 9189. 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 9180*	Lemma for isfin3-2 9189. 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 9181*	Lemma for isfin3-2 9189. 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 9182*	Lemma for isfin3-2 9189. 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 9183*	Lemma for isfin3-2 9189. 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 9184*	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 9185*	Lemma for isfin3-2 9189. Remove hypotheses from isf32lem10 9184. (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 9186*	Lemma for isfin3-2 9189. (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 9187	One half of isfin3-2 9189. (Contributed by Mario Carneiro, 3-Jun-2015.)
|- ( A e. FinIII -> -. om ~<_* A )
Theorem	isf33lem 9188*	Lemma for isfin3-3 9190. (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 9189	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 9190*	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 9191*	Inference from isfin3-3 9190. (This is actually a bit stronger than isfin3-3 9190 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 9192*	Lemma for compsscnv 9193. (Contributed by Mario Carneiro, 17-May-2015.)
|- ( ( x e. ~P A /\ y = ( A \ x ) ) -> ( y e. ~P A /\ x = ( A \ y ) ) )
Theorem	compsscnv 9193*	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 9194*	Lemma for isfin3-4 9204. (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 9195*	Lemma for isfin3-4 9204. (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 9196*	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 9197*	Lemma for isfin3-4 9204. (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 9198*	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 9199*	Lemma for isfin3-4 9204. (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 9200*	Lemma for isfin3-4 9204. (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 ) )