Metamath Proof Explorer

Theorem isf32lem8

Description: Lemma for isfin3-2 . K sets are subsets of the base. (Contributed by Stefan O'Rear, 6-Nov-2014)

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 )
Assertion isf32lem8 
|- ( ( ph /\ A e. _om ) -> ( K ` A ) C_ 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 6 fveq1i 
 |-  ( K ` A ) = ( ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) o. J ) ` A )
8 4 ssrab3 
 |-  S C_ _om
9 1 2 3 4 isf32lem5 
 |-  ( ph -> -. S e. Fin )
10 5 fin23lem22 
 |-  ( ( S C_ _om /\ -. S e. Fin ) -> J : _om -1-1-onto-> S )
11 8 9 10 sylancr 
 |-  ( ph -> J : _om -1-1-onto-> S )
12 f1of 
 |-  ( J : _om -1-1-onto-> S -> J : _om --> S )
13 11 12 syl 
 |-  ( ph -> J : _om --> S )
14 fvco3 
 |-  ( ( J : _om --> S /\ A e. _om ) -> ( ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) o. J ) ` A ) = ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) ` ( J ` A ) ) )
15 13 14 sylan 
 |-  ( ( ph /\ A e. _om ) -> ( ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) o. J ) ` A ) = ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) ` ( J ` A ) ) )
16 13 ffvelrnda 
 |-  ( ( ph /\ A e. _om ) -> ( J ` A ) e. S )
17 fveq2 
 |-  ( w = ( J ` A ) -> ( F ` w ) = ( F ` ( J ` A ) ) )
18 suceq 
 |-  ( w = ( J ` A ) -> suc w = suc ( J ` A ) )
19 18 fveq2d 
 |-  ( w = ( J ` A ) -> ( F ` suc w ) = ( F ` suc ( J ` A ) ) )
20 17 19 difeq12d 
 |-  ( w = ( J ` A ) -> ( ( F ` w ) \ ( F ` suc w ) ) = ( ( F ` ( J ` A ) ) \ ( F ` suc ( J ` A ) ) ) )
21 eqid 
 |-  ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) = ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) )
22 fvex 
 |-  ( F ` ( J ` A ) ) e. _V
23 22 difexi 
 |-  ( ( F ` ( J ` A ) ) \ ( F ` suc ( J ` A ) ) ) e. _V
24 20 21 23 fvmpt 
 |-  ( ( J ` A ) e. S -> ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) ` ( J ` A ) ) = ( ( F ` ( J ` A ) ) \ ( F ` suc ( J ` A ) ) ) )
25 16 24 syl 
 |-  ( ( ph /\ A e. _om ) -> ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) ` ( J ` A ) ) = ( ( F ` ( J ` A ) ) \ ( F ` suc ( J ` A ) ) ) )
26 15 25 eqtrd 
 |-  ( ( ph /\ A e. _om ) -> ( ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) o. J ) ` A ) = ( ( F ` ( J ` A ) ) \ ( F ` suc ( J ` A ) ) ) )
27 7 26 syl5eq 
 |-  ( ( ph /\ A e. _om ) -> ( K ` A ) = ( ( F ` ( J ` A ) ) \ ( F ` suc ( J ` A ) ) ) )
28 1 adantr 
 |-  ( ( ph /\ A e. _om ) -> F : _om --> ~P G )
29 8 16 sseldi 
 |-  ( ( ph /\ A e. _om ) -> ( J ` A ) e. _om )
30 28 29 ffvelrnd 
 |-  ( ( ph /\ A e. _om ) -> ( F ` ( J ` A ) ) e. ~P G )
31 30 elpwid 
 |-  ( ( ph /\ A e. _om ) -> ( F ` ( J ` A ) ) C_ G )
32 31 ssdifssd 
 |-  ( ( ph /\ A e. _om ) -> ( ( F ` ( J ` A ) ) \ ( F ` suc ( J ` A ) ) ) C_ G )
33 27 32 eqsstrd 
 |-  ( ( ph /\ A e. _om ) -> ( K ` A ) C_ G )