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