Metamath Proof Explorer


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