This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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