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