Theorem isf32lem10

Description: 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)

	Ref	Expression
Hypotheses	isf32lem.a	|- ( ph -> F : _om --> ~P G )
	isf32lem.b	|- ( ph -> A. x e. _om ( F ` suc x ) C_ ( F ` x ) )
	isf32lem.c	|- ( ph -> -. |^| ran F e. ran F )
	isf32lem.d	|- S = { y e. _om | ( F ` suc y ) C. ( F ` y ) }
	isf32lem.e	|- J = ( u e. _om |-> ( iota_ v e. S ( v i^i S ) ~~ u ) )
	isf32lem.f	|- K = ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) o. J )
	isf32lem.g	|- L = ( t e. G |-> ( iota s ( s e. _om /\ t e. ( K ` s ) ) ) )
Assertion	isf32lem10	|- ( ph -> ( G e. V -> _om ~<_* G ) )

Proof

Step	Hyp	Ref	Expression
1		isf32lem.a	|- ( ph -> F : _om --> ~P G )
2		isf32lem.b	|- ( ph -> A. x e. _om ( F ` suc x ) C_ ( F ` x ) )
3		isf32lem.c	|- ( ph -> -. |^| ran F e. ran F )
4		isf32lem.d	|- S = { y e. _om | ( F ` suc y ) C. ( F ` y ) }
5		isf32lem.e	|- J = ( u e. _om |-> ( iota_ v e. S ( v i^i S ) ~~ u ) )
6		isf32lem.f	|- K = ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) o. J )
7		isf32lem.g	|- L = ( t e. G |-> ( iota s ( s e. _om /\ t e. ( K ` s ) ) ) )
8	1 2 3 4 5 6 7	isf32lem9	|- ( ph -> L : G -onto-> _om )
9		fof	|- ( L : G -onto-> _om -> L : G --> _om )
10	8 9	syl	|- ( ph -> L : G --> _om )
11		fex	|- ( ( L : G --> _om /\ G e. V ) -> L e. _V )
12	10 11	sylan	|- ( ( ph /\ G e. V ) -> L e. _V )
13	12	ex	|- ( ph -> ( G e. V -> L e. _V ) )
14		fowdom	|- ( ( L e. _V /\ L : G -onto-> _om ) -> _om ~<_* G )
15	14	expcom	|- ( L : G -onto-> _om -> ( L e. _V -> _om ~<_* G ) )
16	8 13 15	sylsyld	|- ( ph -> ( G e. V -> _om ~<_* G ) )