Metamath Proof Explorer

Theorem isercolllem2

Description: Lemma for isercoll . (Contributed by Mario Carneiro, 6-Apr-2015)

Ref Expression
Hypotheses isercoll.z 
|- Z = ( ZZ>= ` M )
isercoll.m 
|- ( ph -> M e. ZZ )
isercoll.g 
|- ( ph -> G : NN --> Z )
isercoll.i 
|- ( ( ph /\ k e. NN ) -> ( G ` k ) < ( G ` ( k + 1 ) ) )
Assertion isercolllem2 
|- ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( 1 ... ( # ` ( G " ( `' G " ( M ... N ) ) ) ) ) = ( `' G " ( M ... N ) ) )

Proof

Step Hyp Ref Expression
1 isercoll.z 
 |-  Z = ( ZZ>= ` M )
2 isercoll.m 
 |-  ( ph -> M e. ZZ )
3 isercoll.g 
 |-  ( ph -> G : NN --> Z )
4 isercoll.i 
 |-  ( ( ph /\ k e. NN ) -> ( G ` k ) < ( G ` ( k + 1 ) ) )
5 elfznn 
 |-  ( x e. ( 1 ... sup ( ( `' G " ( M ... N ) ) , RR , < ) ) -> x e. NN )
6 5 a1i 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( x e. ( 1 ... sup ( ( `' G " ( M ... N ) ) , RR , < ) ) -> x e. NN ) )
7 cnvimass 
 |-  ( `' G " ( M ... N ) ) C_ dom G
8 3 adantr 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> G : NN --> Z )
9 7 8 fssdm 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( `' G " ( M ... N ) ) C_ NN )
10 9 sseld 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( x e. ( `' G " ( M ... N ) ) -> x e. NN ) )
11 id 
 |-  ( x e. NN -> x e. NN )
12 nnuz 
 |-  NN = ( ZZ>= ` 1 )
13 11 12 eleqtrdi 
 |-  ( x e. NN -> x e. ( ZZ>= ` 1 ) )
14 ltso 
 |-  < Or RR
15 14 a1i 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> < Or RR )
16 fzfid 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( M ... N ) e. Fin )
17 ffun 
 |-  ( G : NN --> Z -> Fun G )
18 funimacnv 
 |-  ( Fun G -> ( G " ( `' G " ( M ... N ) ) ) = ( ( M ... N ) i^i ran G ) )
19 8 17 18 3syl 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( G " ( `' G " ( M ... N ) ) ) = ( ( M ... N ) i^i ran G ) )
20 inss1 
 |-  ( ( M ... N ) i^i ran G ) C_ ( M ... N )
21 19 20 eqsstrdi 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( G " ( `' G " ( M ... N ) ) ) C_ ( M ... N ) )
22 16 21 ssfid 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( G " ( `' G " ( M ... N ) ) ) e. Fin )
23 ssid 
 |-  NN C_ NN
24 1 2 3 4 isercolllem1 
 |-  ( ( ph /\ NN C_ NN ) -> ( G |` NN ) Isom < , < ( NN , ( G " NN ) ) )
25 23 24 mpan2 
 |-  ( ph -> ( G |` NN ) Isom < , < ( NN , ( G " NN ) ) )
26 ffn 
 |-  ( G : NN --> Z -> G Fn NN )
27 fnresdm 
 |-  ( G Fn NN -> ( G |` NN ) = G )
28 isoeq1 
 |-  ( ( G |` NN ) = G -> ( ( G |` NN ) Isom < , < ( NN , ( G " NN ) ) <-> G Isom < , < ( NN , ( G " NN ) ) ) )
29 3 26 27 28 4syl 
 |-  ( ph -> ( ( G |` NN ) Isom < , < ( NN , ( G " NN ) ) <-> G Isom < , < ( NN , ( G " NN ) ) ) )
30 25 29 mpbid 
 |-  ( ph -> G Isom < , < ( NN , ( G " NN ) ) )
31 isof1o 
 |-  ( G Isom < , < ( NN , ( G " NN ) ) -> G : NN -1-1-onto-> ( G " NN ) )
32 f1ocnv 
 |-  ( G : NN -1-1-onto-> ( G " NN ) -> `' G : ( G " NN ) -1-1-onto-> NN )
33 f1ofun 
 |-  ( `' G : ( G " NN ) -1-1-onto-> NN -> Fun `' G )
34 30 31 32 33 4syl 
 |-  ( ph -> Fun `' G )
35 df-f1 
 |-  ( G : NN -1-1-> Z <-> ( G : NN --> Z /\ Fun `' G ) )
36 3 34 35 sylanbrc 
 |-  ( ph -> G : NN -1-1-> Z )
37 36 adantr 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> G : NN -1-1-> Z )
38 nnex 
 |-  NN e. _V
39 ssexg 
 |-  ( ( ( `' G " ( M ... N ) ) C_ NN /\ NN e. _V ) -> ( `' G " ( M ... N ) ) e. _V )
40 9 38 39 sylancl 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( `' G " ( M ... N ) ) e. _V )
41 f1imaeng 
 |-  ( ( G : NN -1-1-> Z /\ ( `' G " ( M ... N ) ) C_ NN /\ ( `' G " ( M ... N ) ) e. _V ) -> ( G " ( `' G " ( M ... N ) ) ) ~~ ( `' G " ( M ... N ) ) )
42 37 9 40 41 syl3anc 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( G " ( `' G " ( M ... N ) ) ) ~~ ( `' G " ( M ... N ) ) )
43 42 ensymd 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( `' G " ( M ... N ) ) ~~ ( G " ( `' G " ( M ... N ) ) ) )
44 enfii 
 |-  ( ( ( G " ( `' G " ( M ... N ) ) ) e. Fin /\ ( `' G " ( M ... N ) ) ~~ ( G " ( `' G " ( M ... N ) ) ) ) -> ( `' G " ( M ... N ) ) e. Fin )
45 22 43 44 syl2anc 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( `' G " ( M ... N ) ) e. Fin )
46 1nn 
 |-  1 e. NN
47 46 a1i 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> 1 e. NN )
48 ffvelrn 
 |-  ( ( G : NN --> Z /\ 1 e. NN ) -> ( G ` 1 ) e. Z )
49 3 46 48 sylancl 
 |-  ( ph -> ( G ` 1 ) e. Z )
50 49 1 eleqtrdi 
 |-  ( ph -> ( G ` 1 ) e. ( ZZ>= ` M ) )
51 50 adantr 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( G ` 1 ) e. ( ZZ>= ` M ) )
52 simpr 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> N e. ( ZZ>= ` ( G ` 1 ) ) )
53 elfzuzb 
 |-  ( ( G ` 1 ) e. ( M ... N ) <-> ( ( G ` 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) )
54 51 52 53 sylanbrc 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( G ` 1 ) e. ( M ... N ) )
55 8 ffnd 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> G Fn NN )
56 elpreima 
 |-  ( G Fn NN -> ( 1 e. ( `' G " ( M ... N ) ) <-> ( 1 e. NN /\ ( G ` 1 ) e. ( M ... N ) ) ) )
57 55 56 syl 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( 1 e. ( `' G " ( M ... N ) ) <-> ( 1 e. NN /\ ( G ` 1 ) e. ( M ... N ) ) ) )
58 47 54 57 mpbir2and 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> 1 e. ( `' G " ( M ... N ) ) )
59 58 ne0d 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( `' G " ( M ... N ) ) =/= (/) )
60 nnssre 
 |-  NN C_ RR
61 9 60 sstrdi 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( `' G " ( M ... N ) ) C_ RR )
62 fisupcl 
 |-  ( ( < Or RR /\ ( ( `' G " ( M ... N ) ) e. Fin /\ ( `' G " ( M ... N ) ) =/= (/) /\ ( `' G " ( M ... N ) ) C_ RR ) ) -> sup ( ( `' G " ( M ... N ) ) , RR , < ) e. ( `' G " ( M ... N ) ) )
63 15 45 59 61 62 syl13anc 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> sup ( ( `' G " ( M ... N ) ) , RR , < ) e. ( `' G " ( M ... N ) ) )
64 9 63 sseldd 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> sup ( ( `' G " ( M ... N ) ) , RR , < ) e. NN )
65 64 nnzd 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> sup ( ( `' G " ( M ... N ) ) , RR , < ) e. ZZ )
66 elfz5 
 |-  ( ( x e. ( ZZ>= ` 1 ) /\ sup ( ( `' G " ( M ... N ) ) , RR , < ) e. ZZ ) -> ( x e. ( 1 ... sup ( ( `' G " ( M ... N ) ) , RR , < ) ) <-> x <_ sup ( ( `' G " ( M ... N ) ) , RR , < ) ) )
67 13 65 66 syl2anr 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ x e. NN ) -> ( x e. ( 1 ... sup ( ( `' G " ( M ... N ) ) , RR , < ) ) <-> x <_ sup ( ( `' G " ( M ... N ) ) , RR , < ) ) )
68 elpreima 
 |-  ( G Fn NN -> ( sup ( ( `' G " ( M ... N ) ) , RR , < ) e. ( `' G " ( M ... N ) ) <-> ( sup ( ( `' G " ( M ... N ) ) , RR , < ) e. NN /\ ( G ` sup ( ( `' G " ( M ... N ) ) , RR , < ) ) e. ( M ... N ) ) ) )
69 55 68 syl 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( sup ( ( `' G " ( M ... N ) ) , RR , < ) e. ( `' G " ( M ... N ) ) <-> ( sup ( ( `' G " ( M ... N ) ) , RR , < ) e. NN /\ ( G ` sup ( ( `' G " ( M ... N ) ) , RR , < ) ) e. ( M ... N ) ) ) )
70 63 69 mpbid 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( sup ( ( `' G " ( M ... N ) ) , RR , < ) e. NN /\ ( G ` sup ( ( `' G " ( M ... N ) ) , RR , < ) ) e. ( M ... N ) ) )
71 elfzle2 
 |-  ( ( G ` sup ( ( `' G " ( M ... N ) ) , RR , < ) ) e. ( M ... N ) -> ( G ` sup ( ( `' G " ( M ... N ) ) , RR , < ) ) <_ N )
72 70 71 simpl2im 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( G ` sup ( ( `' G " ( M ... N ) ) , RR , < ) ) <_ N )
73 72 adantr 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ x e. NN ) -> ( G ` sup ( ( `' G " ( M ... N ) ) , RR , < ) ) <_ N )
74 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
75 1 74 eqsstri 
 |-  Z C_ ZZ
76 zssre 
 |-  ZZ C_ RR
77 75 76 sstri 
 |-  Z C_ RR
78 8 ffvelrnda 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ x e. NN ) -> ( G ` x ) e. Z )
79 77 78 sseldi 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ x e. NN ) -> ( G ` x ) e. RR )
80 8 64 ffvelrnd 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( G ` sup ( ( `' G " ( M ... N ) ) , RR , < ) ) e. Z )
81 80 adantr 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ x e. NN ) -> ( G ` sup ( ( `' G " ( M ... N ) ) , RR , < ) ) e. Z )
82 77 81 sseldi 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ x e. NN ) -> ( G ` sup ( ( `' G " ( M ... N ) ) , RR , < ) ) e. RR )
83 eluzelz 
 |-  ( N e. ( ZZ>= ` ( G ` 1 ) ) -> N e. ZZ )
84 83 ad2antlr 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ x e. NN ) -> N e. ZZ )
85 76 84 sseldi 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ x e. NN ) -> N e. RR )
86 letr 
 |-  ( ( ( G ` x ) e. RR /\ ( G ` sup ( ( `' G " ( M ... N ) ) , RR , < ) ) e. RR /\ N e. RR ) -> ( ( ( G ` x ) <_ ( G ` sup ( ( `' G " ( M ... N ) ) , RR , < ) ) /\ ( G ` sup ( ( `' G " ( M ... N ) ) , RR , < ) ) <_ N ) -> ( G ` x ) <_ N ) )
87 79 82 85 86 syl3anc 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ x e. NN ) -> ( ( ( G ` x ) <_ ( G ` sup ( ( `' G " ( M ... N ) ) , RR , < ) ) /\ ( G ` sup ( ( `' G " ( M ... N ) ) , RR , < ) ) <_ N ) -> ( G ` x ) <_ N ) )
88 73 87 mpan2d 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ x e. NN ) -> ( ( G ` x ) <_ ( G ` sup ( ( `' G " ( M ... N ) ) , RR , < ) ) -> ( G ` x ) <_ N ) )
89 30 ad2antrr 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ x e. NN ) -> G Isom < , < ( NN , ( G " NN ) ) )
90 60 a1i 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ x e. NN ) -> NN C_ RR )
91 ressxr 
 |-  RR C_ RR*
92 90 91 sstrdi 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ x e. NN ) -> NN C_ RR* )
93 imassrn 
 |-  ( G " NN ) C_ ran G
94 3 ad2antrr 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ x e. NN ) -> G : NN --> Z )
95 94 frnd 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ x e. NN ) -> ran G C_ Z )
96 93 95 sstrid 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ x e. NN ) -> ( G " NN ) C_ Z )
97 96 77 sstrdi 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ x e. NN ) -> ( G " NN ) C_ RR )
98 97 91 sstrdi 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ x e. NN ) -> ( G " NN ) C_ RR* )
99 simpr 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ x e. NN ) -> x e. NN )
100 64 adantr 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ x e. NN ) -> sup ( ( `' G " ( M ... N ) ) , RR , < ) e. NN )
101 leisorel 
 |-  ( ( G Isom < , < ( NN , ( G " NN ) ) /\ ( NN C_ RR* /\ ( G " NN ) C_ RR* ) /\ ( x e. NN /\ sup ( ( `' G " ( M ... N ) ) , RR , < ) e. NN ) ) -> ( x <_ sup ( ( `' G " ( M ... N ) ) , RR , < ) <-> ( G ` x ) <_ ( G ` sup ( ( `' G " ( M ... N ) ) , RR , < ) ) ) )
102 89 92 98 99 100 101 syl122anc 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ x e. NN ) -> ( x <_ sup ( ( `' G " ( M ... N ) ) , RR , < ) <-> ( G ` x ) <_ ( G ` sup ( ( `' G " ( M ... N ) ) , RR , < ) ) ) )
103 78 1 eleqtrdi 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ x e. NN ) -> ( G ` x ) e. ( ZZ>= ` M ) )
104 elfz5 
 |-  ( ( ( G ` x ) e. ( ZZ>= ` M ) /\ N e. ZZ ) -> ( ( G ` x ) e. ( M ... N ) <-> ( G ` x ) <_ N ) )
105 103 84 104 syl2anc 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ x e. NN ) -> ( ( G ` x ) e. ( M ... N ) <-> ( G ` x ) <_ N ) )
106 88 102 105 3imtr4d 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ x e. NN ) -> ( x <_ sup ( ( `' G " ( M ... N ) ) , RR , < ) -> ( G ` x ) e. ( M ... N ) ) )
107 elpreima 
 |-  ( G Fn NN -> ( x e. ( `' G " ( M ... N ) ) <-> ( x e. NN /\ ( G ` x ) e. ( M ... N ) ) ) )
108 107 baibd 
 |-  ( ( G Fn NN /\ x e. NN ) -> ( x e. ( `' G " ( M ... N ) ) <-> ( G ` x ) e. ( M ... N ) ) )
109 55 108 sylan 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ x e. NN ) -> ( x e. ( `' G " ( M ... N ) ) <-> ( G ` x ) e. ( M ... N ) ) )
110 106 109 sylibrd 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ x e. NN ) -> ( x <_ sup ( ( `' G " ( M ... N ) ) , RR , < ) -> x e. ( `' G " ( M ... N ) ) ) )
111 fimaxre2 
 |-  ( ( ( `' G " ( M ... N ) ) C_ RR /\ ( `' G " ( M ... N ) ) e. Fin ) -> E. x e. RR A. y e. ( `' G " ( M ... N ) ) y <_ x )
112 61 45 111 syl2anc 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> E. x e. RR A. y e. ( `' G " ( M ... N ) ) y <_ x )
113 suprub 
 |-  ( ( ( ( `' G " ( M ... N ) ) C_ RR /\ ( `' G " ( M ... N ) ) =/= (/) /\ E. x e. RR A. y e. ( `' G " ( M ... N ) ) y <_ x ) /\ x e. ( `' G " ( M ... N ) ) ) -> x <_ sup ( ( `' G " ( M ... N ) ) , RR , < ) )
114 113 ex 
 |-  ( ( ( `' G " ( M ... N ) ) C_ RR /\ ( `' G " ( M ... N ) ) =/= (/) /\ E. x e. RR A. y e. ( `' G " ( M ... N ) ) y <_ x ) -> ( x e. ( `' G " ( M ... N ) ) -> x <_ sup ( ( `' G " ( M ... N ) ) , RR , < ) ) )
115 61 59 112 114 syl3anc 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( x e. ( `' G " ( M ... N ) ) -> x <_ sup ( ( `' G " ( M ... N ) ) , RR , < ) ) )
116 115 adantr 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ x e. NN ) -> ( x e. ( `' G " ( M ... N ) ) -> x <_ sup ( ( `' G " ( M ... N ) ) , RR , < ) ) )
117 110 116 impbid 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ x e. NN ) -> ( x <_ sup ( ( `' G " ( M ... N ) ) , RR , < ) <-> x e. ( `' G " ( M ... N ) ) ) )
118 67 117 bitrd 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ x e. NN ) -> ( x e. ( 1 ... sup ( ( `' G " ( M ... N ) ) , RR , < ) ) <-> x e. ( `' G " ( M ... N ) ) ) )
119 118 ex 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( x e. NN -> ( x e. ( 1 ... sup ( ( `' G " ( M ... N ) ) , RR , < ) ) <-> x e. ( `' G " ( M ... N ) ) ) ) )
120 6 10 119 pm5.21ndd 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( x e. ( 1 ... sup ( ( `' G " ( M ... N ) ) , RR , < ) ) <-> x e. ( `' G " ( M ... N ) ) ) )
121 120 eqrdv 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( 1 ... sup ( ( `' G " ( M ... N ) ) , RR , < ) ) = ( `' G " ( M ... N ) ) )
122 121 fveq2d 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( # ` ( 1 ... sup ( ( `' G " ( M ... N ) ) , RR , < ) ) ) = ( # ` ( `' G " ( M ... N ) ) ) )
123 64 nnnn0d 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> sup ( ( `' G " ( M ... N ) ) , RR , < ) e. NN0 )
124 hashfz1 
 |-  ( sup ( ( `' G " ( M ... N ) ) , RR , < ) e. NN0 -> ( # ` ( 1 ... sup ( ( `' G " ( M ... N ) ) , RR , < ) ) ) = sup ( ( `' G " ( M ... N ) ) , RR , < ) )
125 123 124 syl 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( # ` ( 1 ... sup ( ( `' G " ( M ... N ) ) , RR , < ) ) ) = sup ( ( `' G " ( M ... N ) ) , RR , < ) )
126 hashen 
 |-  ( ( ( `' G " ( M ... N ) ) e. Fin /\ ( G " ( `' G " ( M ... N ) ) ) e. Fin ) -> ( ( # ` ( `' G " ( M ... N ) ) ) = ( # ` ( G " ( `' G " ( M ... N ) ) ) ) <-> ( `' G " ( M ... N ) ) ~~ ( G " ( `' G " ( M ... N ) ) ) ) )
127 45 22 126 syl2anc 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( ( # ` ( `' G " ( M ... N ) ) ) = ( # ` ( G " ( `' G " ( M ... N ) ) ) ) <-> ( `' G " ( M ... N ) ) ~~ ( G " ( `' G " ( M ... N ) ) ) ) )
128 43 127 mpbird 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( # ` ( `' G " ( M ... N ) ) ) = ( # ` ( G " ( `' G " ( M ... N ) ) ) ) )
129 122 125 128 3eqtr3d 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> sup ( ( `' G " ( M ... N ) ) , RR , < ) = ( # ` ( G " ( `' G " ( M ... N ) ) ) ) )
130 129 oveq2d 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( 1 ... sup ( ( `' G " ( M ... N ) ) , RR , < ) ) = ( 1 ... ( # ` ( G " ( `' G " ( M ... N ) ) ) ) ) )
131 130 121 eqtr3d 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( 1 ... ( # ` ( G " ( `' G " ( M ... N ) ) ) ) ) = ( `' G " ( M ... N ) ) )