Metamath Proof Explorer

Theorem isf32lem6

Description: Lemma for isfin3-2 . Each K value is nonempty. (Contributed by Stefan O'Rear, 5-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 isf32lem6 
|- ( ( ph /\ A e. _om ) -> ( K ` A ) =/= (/) )

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 9 adantr 
 |-  ( ( ph /\ A e. _om ) -> -. S e. Fin )
17 8 16 10 sylancr 
 |-  ( ( ph /\ A e. _om ) -> J : _om -1-1-onto-> S )
18 17 12 syl 
 |-  ( ( ph /\ A e. _om ) -> J : _om --> S )
19 ffvelrn 
 |-  ( ( J : _om --> S /\ A e. _om ) -> ( J ` A ) e. S )
20 18 19 sylancom 
 |-  ( ( ph /\ A e. _om ) -> ( J ` A ) e. S )
21 fveq2 
 |-  ( w = ( J ` A ) -> ( F ` w ) = ( F ` ( J ` A ) ) )
22 suceq 
 |-  ( w = ( J ` A ) -> suc w = suc ( J ` A ) )
23 22 fveq2d 
 |-  ( w = ( J ` A ) -> ( F ` suc w ) = ( F ` suc ( J ` A ) ) )
24 21 23 difeq12d 
 |-  ( w = ( J ` A ) -> ( ( F ` w ) \ ( F ` suc w ) ) = ( ( F ` ( J ` A ) ) \ ( F ` suc ( J ` A ) ) ) )
25 eqid 
 |-  ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) = ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) )
26 fvex 
 |-  ( F ` ( J ` A ) ) e. _V
27 26 difexi 
 |-  ( ( F ` ( J ` A ) ) \ ( F ` suc ( J ` A ) ) ) e. _V
28 24 25 27 fvmpt 
 |-  ( ( J ` A ) e. S -> ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) ` ( J ` A ) ) = ( ( F ` ( J ` A ) ) \ ( F ` suc ( J ` A ) ) ) )
29 20 28 syl 
 |-  ( ( ph /\ A e. _om ) -> ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) ` ( J ` A ) ) = ( ( F ` ( J ` A ) ) \ ( F ` suc ( J ` A ) ) ) )
30 15 29 eqtrd 
 |-  ( ( ph /\ A e. _om ) -> ( ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) o. J ) ` A ) = ( ( F ` ( J ` A ) ) \ ( F ` suc ( J ` A ) ) ) )
31 7 30 syl5eq 
 |-  ( ( ph /\ A e. _om ) -> ( K ` A ) = ( ( F ` ( J ` A ) ) \ ( F ` suc ( J ` A ) ) ) )
32 suceq 
 |-  ( y = ( J ` A ) -> suc y = suc ( J ` A ) )
33 32 fveq2d 
 |-  ( y = ( J ` A ) -> ( F ` suc y ) = ( F ` suc ( J ` A ) ) )
34 fveq2 
 |-  ( y = ( J ` A ) -> ( F ` y ) = ( F ` ( J ` A ) ) )
35 33 34 psseq12d 
 |-  ( y = ( J ` A ) -> ( ( F ` suc y ) C. ( F ` y ) <-> ( F ` suc ( J ` A ) ) C. ( F ` ( J ` A ) ) ) )
36 35 4 elrab2 
 |-  ( ( J ` A ) e. S <-> ( ( J ` A ) e. _om /\ ( F ` suc ( J ` A ) ) C. ( F ` ( J ` A ) ) ) )
37 36 simprbi 
 |-  ( ( J ` A ) e. S -> ( F ` suc ( J ` A ) ) C. ( F ` ( J ` A ) ) )
38 20 37 syl 
 |-  ( ( ph /\ A e. _om ) -> ( F ` suc ( J ` A ) ) C. ( F ` ( J ` A ) ) )
39 df-pss 
 |-  ( ( F ` suc ( J ` A ) ) C. ( F ` ( J ` A ) ) <-> ( ( F ` suc ( J ` A ) ) C_ ( F ` ( J ` A ) ) /\ ( F ` suc ( J ` A ) ) =/= ( F ` ( J ` A ) ) ) )
40 38 39 sylib 
 |-  ( ( ph /\ A e. _om ) -> ( ( F ` suc ( J ` A ) ) C_ ( F ` ( J ` A ) ) /\ ( F ` suc ( J ` A ) ) =/= ( F ` ( J ` A ) ) ) )
41 pssdifn0 
 |-  ( ( ( F ` suc ( J ` A ) ) C_ ( F ` ( J ` A ) ) /\ ( F ` suc ( J ` A ) ) =/= ( F ` ( J ` A ) ) ) -> ( ( F ` ( J ` A ) ) \ ( F ` suc ( J ` A ) ) ) =/= (/) )
42 40 41 syl 
 |-  ( ( ph /\ A e. _om ) -> ( ( F ` ( J ` A ) ) \ ( F ` suc ( J ` A ) ) ) =/= (/) )
43 31 42 eqnetrd 
 |-  ( ( ph /\ A e. _om ) -> ( K ` A ) =/= (/) )