Metamath Proof Explorer

Theorem isf32lem7

Description: Lemma for isfin3-2 . Different K values are disjoint. (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 isf32lem7 
|- ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) -> ( ( K ` A ) i^i ( K ` B ) ) = (/) )

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 15 ad2ant2r 
 |-  ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) -> ( ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) o. J ) ` A ) = ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) ` ( J ` A ) ) )
17 13 adantr 
 |-  ( ( ph /\ A =/= B ) -> J : _om --> S )
18 simpl 
 |-  ( ( A e. _om /\ B e. _om ) -> A e. _om )
19 ffvelcdm 
 |-  ( ( J : _om --> S /\ A e. _om ) -> ( J ` A ) e. S )
20 17 18 19 syl2an 
 |-  ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B 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 =/= B ) /\ ( A e. _om /\ B e. _om ) ) -> ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) ` ( J ` A ) ) = ( ( F ` ( J ` A ) ) \ ( F ` suc ( J ` A ) ) ) )
30 16 29 eqtrd 
 |-  ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) -> ( ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) o. J ) ` A ) = ( ( F ` ( J ` A ) ) \ ( F ` suc ( J ` A ) ) ) )
31 7 30 eqtrid 
 |-  ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) -> ( K ` A ) = ( ( F ` ( J ` A ) ) \ ( F ` suc ( J ` A ) ) ) )
32 6 fveq1i 
 |-  ( K ` B ) = ( ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) o. J ) ` B )
33 fvco3 
 |-  ( ( J : _om --> S /\ B e. _om ) -> ( ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) o. J ) ` B ) = ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) ` ( J ` B ) ) )
34 13 33 sylan 
 |-  ( ( ph /\ B e. _om ) -> ( ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) o. J ) ` B ) = ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) ` ( J ` B ) ) )
35 34 ad2ant2rl 
 |-  ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) -> ( ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) o. J ) ` B ) = ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) ` ( J ` B ) ) )
36 simpr 
 |-  ( ( A e. _om /\ B e. _om ) -> B e. _om )
37 ffvelcdm 
 |-  ( ( J : _om --> S /\ B e. _om ) -> ( J ` B ) e. S )
38 17 36 37 syl2an 
 |-  ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) -> ( J ` B ) e. S )
39 fveq2 
 |-  ( w = ( J ` B ) -> ( F ` w ) = ( F ` ( J ` B ) ) )
40 suceq 
 |-  ( w = ( J ` B ) -> suc w = suc ( J ` B ) )
41 40 fveq2d 
 |-  ( w = ( J ` B ) -> ( F ` suc w ) = ( F ` suc ( J ` B ) ) )
42 39 41 difeq12d 
 |-  ( w = ( J ` B ) -> ( ( F ` w ) \ ( F ` suc w ) ) = ( ( F ` ( J ` B ) ) \ ( F ` suc ( J ` B ) ) ) )
43 fvex 
 |-  ( F ` ( J ` B ) ) e. _V
44 43 difexi 
 |-  ( ( F ` ( J ` B ) ) \ ( F ` suc ( J ` B ) ) ) e. _V
45 42 25 44 fvmpt 
 |-  ( ( J ` B ) e. S -> ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) ` ( J ` B ) ) = ( ( F ` ( J ` B ) ) \ ( F ` suc ( J ` B ) ) ) )
46 38 45 syl 
 |-  ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) -> ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) ` ( J ` B ) ) = ( ( F ` ( J ` B ) ) \ ( F ` suc ( J ` B ) ) ) )
47 35 46 eqtrd 
 |-  ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) -> ( ( ( w e. S |-> ( ( F ` w ) \ ( F ` suc w ) ) ) o. J ) ` B ) = ( ( F ` ( J ` B ) ) \ ( F ` suc ( J ` B ) ) ) )
48 32 47 eqtrid 
 |-  ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) -> ( K ` B ) = ( ( F ` ( J ` B ) ) \ ( F ` suc ( J ` B ) ) ) )
49 31 48 ineq12d 
 |-  ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) -> ( ( K ` A ) i^i ( K ` B ) ) = ( ( ( F ` ( J ` A ) ) \ ( F ` suc ( J ` A ) ) ) i^i ( ( F ` ( J ` B ) ) \ ( F ` suc ( J ` B ) ) ) ) )
50 simpll 
 |-  ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) -> ph )
51 simplr 
 |-  ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) -> A =/= B )
52 f1of1 
 |-  ( J : _om -1-1-onto-> S -> J : _om -1-1-> S )
53 11 52 syl 
 |-  ( ph -> J : _om -1-1-> S )
54 53 adantr 
 |-  ( ( ph /\ A =/= B ) -> J : _om -1-1-> S )
55 f1fveq 
 |-  ( ( J : _om -1-1-> S /\ ( A e. _om /\ B e. _om ) ) -> ( ( J ` A ) = ( J ` B ) <-> A = B ) )
56 54 55 sylan 
 |-  ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) -> ( ( J ` A ) = ( J ` B ) <-> A = B ) )
57 56 biimpd 
 |-  ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) -> ( ( J ` A ) = ( J ` B ) -> A = B ) )
58 57 necon3d 
 |-  ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) -> ( A =/= B -> ( J ` A ) =/= ( J ` B ) ) )
59 51 58 mpd 
 |-  ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) -> ( J ` A ) =/= ( J ` B ) )
60 8 20 sselid 
 |-  ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) -> ( J ` A ) e. _om )
61 8 38 sselid 
 |-  ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) -> ( J ` B ) e. _om )
62 1 2 3 isf32lem4 
 |-  ( ( ( ph /\ ( J ` A ) =/= ( J ` B ) ) /\ ( ( J ` A ) e. _om /\ ( J ` B ) e. _om ) ) -> ( ( ( F ` ( J ` A ) ) \ ( F ` suc ( J ` A ) ) ) i^i ( ( F ` ( J ` B ) ) \ ( F ` suc ( J ` B ) ) ) ) = (/) )
63 50 59 60 61 62 syl22anc 
 |-  ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) -> ( ( ( F ` ( J ` A ) ) \ ( F ` suc ( J ` A ) ) ) i^i ( ( F ` ( J ` B ) ) \ ( F ` suc ( J ` B ) ) ) ) = (/) )
64 49 63 eqtrd 
 |-  ( ( ( ph /\ A =/= B ) /\ ( A e. _om /\ B e. _om ) ) -> ( ( K ` A ) i^i ( K ` B ) ) = (/) )