Step |
Hyp |
Ref |
Expression |
1 |
|
smfinflem.m |
|- ( ph -> M e. ZZ ) |
2 |
|
smfinflem.z |
|- Z = ( ZZ>= ` M ) |
3 |
|
smfinflem.s |
|- ( ph -> S e. SAlg ) |
4 |
|
smfinflem.f |
|- ( ph -> F : Z --> ( SMblFn ` S ) ) |
5 |
|
smfinflem.d |
|- D = { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) } |
6 |
|
smfinflem.g |
|- G = ( x e. D |-> inf ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) ) |
7 |
6
|
a1i |
|- ( ph -> G = ( x e. D |-> inf ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) ) ) |
8 |
|
nfv |
|- F/ n ( ph /\ x e. D ) |
9 |
1 2
|
uzn0d |
|- ( ph -> Z =/= (/) ) |
10 |
9
|
adantr |
|- ( ( ph /\ x e. D ) -> Z =/= (/) ) |
11 |
3
|
adantr |
|- ( ( ph /\ n e. Z ) -> S e. SAlg ) |
12 |
4
|
ffvelrnda |
|- ( ( ph /\ n e. Z ) -> ( F ` n ) e. ( SMblFn ` S ) ) |
13 |
|
eqid |
|- dom ( F ` n ) = dom ( F ` n ) |
14 |
11 12 13
|
smff |
|- ( ( ph /\ n e. Z ) -> ( F ` n ) : dom ( F ` n ) --> RR ) |
15 |
14
|
adantlr |
|- ( ( ( ph /\ x e. D ) /\ n e. Z ) -> ( F ` n ) : dom ( F ` n ) --> RR ) |
16 |
|
ssrab2 |
|- { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) } C_ |^|_ n e. Z dom ( F ` n ) |
17 |
5
|
eleq2i |
|- ( x e. D <-> x e. { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) } ) |
18 |
17
|
biimpi |
|- ( x e. D -> x e. { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) } ) |
19 |
16 18
|
sseldi |
|- ( x e. D -> x e. |^|_ n e. Z dom ( F ` n ) ) |
20 |
19
|
adantr |
|- ( ( x e. D /\ n e. Z ) -> x e. |^|_ n e. Z dom ( F ` n ) ) |
21 |
|
simpr |
|- ( ( x e. D /\ n e. Z ) -> n e. Z ) |
22 |
|
eliinid |
|- ( ( x e. |^|_ n e. Z dom ( F ` n ) /\ n e. Z ) -> x e. dom ( F ` n ) ) |
23 |
20 21 22
|
syl2anc |
|- ( ( x e. D /\ n e. Z ) -> x e. dom ( F ` n ) ) |
24 |
23
|
adantll |
|- ( ( ( ph /\ x e. D ) /\ n e. Z ) -> x e. dom ( F ` n ) ) |
25 |
15 24
|
ffvelrnd |
|- ( ( ( ph /\ x e. D ) /\ n e. Z ) -> ( ( F ` n ) ` x ) e. RR ) |
26 |
|
rabidim2 |
|- ( x e. { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) } -> E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) ) |
27 |
18 26
|
syl |
|- ( x e. D -> E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) ) |
28 |
27
|
adantl |
|- ( ( ph /\ x e. D ) -> E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) ) |
29 |
8 10 25 28
|
infnsuprnmpt |
|- ( ( ph /\ x e. D ) -> inf ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) = -u sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) ) |
30 |
29
|
mpteq2dva |
|- ( ph -> ( x e. D |-> inf ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) ) = ( x e. D |-> -u sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) ) ) |
31 |
7 30
|
eqtrd |
|- ( ph -> G = ( x e. D |-> -u sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) ) ) |
32 |
|
nfv |
|- F/ x ph |
33 |
|
fvex |
|- ( F ` n ) e. _V |
34 |
33
|
dmex |
|- dom ( F ` n ) e. _V |
35 |
34
|
rgenw |
|- A. n e. Z dom ( F ` n ) e. _V |
36 |
35
|
a1i |
|- ( ph -> A. n e. Z dom ( F ` n ) e. _V ) |
37 |
9 36
|
iinexd |
|- ( ph -> |^|_ n e. Z dom ( F ` n ) e. _V ) |
38 |
5 37
|
rabexd |
|- ( ph -> D e. _V ) |
39 |
25
|
renegcld |
|- ( ( ( ph /\ x e. D ) /\ n e. Z ) -> -u ( ( F ` n ) ` x ) e. RR ) |
40 |
|
fveq2 |
|- ( w = x -> ( ( F ` m ) ` w ) = ( ( F ` m ) ` x ) ) |
41 |
40
|
breq2d |
|- ( w = x -> ( z <_ ( ( F ` m ) ` w ) <-> z <_ ( ( F ` m ) ` x ) ) ) |
42 |
41
|
ralbidv |
|- ( w = x -> ( A. m e. Z z <_ ( ( F ` m ) ` w ) <-> A. m e. Z z <_ ( ( F ` m ) ` x ) ) ) |
43 |
42
|
rexbidv |
|- ( w = x -> ( E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` w ) <-> E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` x ) ) ) |
44 |
|
nfcv |
|- F/_ w |^|_ n e. Z dom ( F ` n ) |
45 |
|
nfcv |
|- F/_ x Z |
46 |
|
nfcv |
|- F/_ x ( F ` m ) |
47 |
46
|
nfdm |
|- F/_ x dom ( F ` m ) |
48 |
45 47
|
nfiin |
|- F/_ x |^|_ m e. Z dom ( F ` m ) |
49 |
|
nfv |
|- F/ w E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) |
50 |
|
nfv |
|- F/ x E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` w ) |
51 |
|
nfcv |
|- F/_ m dom ( F ` n ) |
52 |
|
nfcv |
|- F/_ n ( F ` m ) |
53 |
52
|
nfdm |
|- F/_ n dom ( F ` m ) |
54 |
|
fveq2 |
|- ( n = m -> ( F ` n ) = ( F ` m ) ) |
55 |
54
|
dmeqd |
|- ( n = m -> dom ( F ` n ) = dom ( F ` m ) ) |
56 |
51 53 55
|
cbviin |
|- |^|_ n e. Z dom ( F ` n ) = |^|_ m e. Z dom ( F ` m ) |
57 |
56
|
a1i |
|- ( x = w -> |^|_ n e. Z dom ( F ` n ) = |^|_ m e. Z dom ( F ` m ) ) |
58 |
|
fveq2 |
|- ( x = w -> ( ( F ` n ) ` x ) = ( ( F ` n ) ` w ) ) |
59 |
58
|
breq2d |
|- ( x = w -> ( y <_ ( ( F ` n ) ` x ) <-> y <_ ( ( F ` n ) ` w ) ) ) |
60 |
59
|
ralbidv |
|- ( x = w -> ( A. n e. Z y <_ ( ( F ` n ) ` x ) <-> A. n e. Z y <_ ( ( F ` n ) ` w ) ) ) |
61 |
|
nfv |
|- F/ m y <_ ( ( F ` n ) ` w ) |
62 |
|
nfcv |
|- F/_ n y |
63 |
|
nfcv |
|- F/_ n <_ |
64 |
|
nfcv |
|- F/_ n w |
65 |
52 64
|
nffv |
|- F/_ n ( ( F ` m ) ` w ) |
66 |
62 63 65
|
nfbr |
|- F/ n y <_ ( ( F ` m ) ` w ) |
67 |
54
|
fveq1d |
|- ( n = m -> ( ( F ` n ) ` w ) = ( ( F ` m ) ` w ) ) |
68 |
67
|
breq2d |
|- ( n = m -> ( y <_ ( ( F ` n ) ` w ) <-> y <_ ( ( F ` m ) ` w ) ) ) |
69 |
61 66 68
|
cbvralw |
|- ( A. n e. Z y <_ ( ( F ` n ) ` w ) <-> A. m e. Z y <_ ( ( F ` m ) ` w ) ) |
70 |
69
|
a1i |
|- ( x = w -> ( A. n e. Z y <_ ( ( F ` n ) ` w ) <-> A. m e. Z y <_ ( ( F ` m ) ` w ) ) ) |
71 |
60 70
|
bitrd |
|- ( x = w -> ( A. n e. Z y <_ ( ( F ` n ) ` x ) <-> A. m e. Z y <_ ( ( F ` m ) ` w ) ) ) |
72 |
71
|
rexbidv |
|- ( x = w -> ( E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) <-> E. y e. RR A. m e. Z y <_ ( ( F ` m ) ` w ) ) ) |
73 |
|
breq1 |
|- ( y = z -> ( y <_ ( ( F ` m ) ` w ) <-> z <_ ( ( F ` m ) ` w ) ) ) |
74 |
73
|
ralbidv |
|- ( y = z -> ( A. m e. Z y <_ ( ( F ` m ) ` w ) <-> A. m e. Z z <_ ( ( F ` m ) ` w ) ) ) |
75 |
74
|
cbvrexvw |
|- ( E. y e. RR A. m e. Z y <_ ( ( F ` m ) ` w ) <-> E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` w ) ) |
76 |
75
|
a1i |
|- ( x = w -> ( E. y e. RR A. m e. Z y <_ ( ( F ` m ) ` w ) <-> E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` w ) ) ) |
77 |
72 76
|
bitrd |
|- ( x = w -> ( E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) <-> E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` w ) ) ) |
78 |
44 48 49 50 57 77
|
cbvrabcsfw |
|- { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) } = { w e. |^|_ m e. Z dom ( F ` m ) | E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` w ) } |
79 |
5 78
|
eqtri |
|- D = { w e. |^|_ m e. Z dom ( F ` m ) | E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` w ) } |
80 |
43 79
|
elrab2 |
|- ( x e. D <-> ( x e. |^|_ m e. Z dom ( F ` m ) /\ E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` x ) ) ) |
81 |
80
|
biimpi |
|- ( x e. D -> ( x e. |^|_ m e. Z dom ( F ` m ) /\ E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` x ) ) ) |
82 |
81
|
simprd |
|- ( x e. D -> E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` x ) ) |
83 |
82
|
adantl |
|- ( ( ph /\ x e. D ) -> E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` x ) ) |
84 |
|
renegcl |
|- ( z e. RR -> -u z e. RR ) |
85 |
84
|
ad2antlr |
|- ( ( ( ( ph /\ x e. D ) /\ z e. RR ) /\ A. m e. Z z <_ ( ( F ` m ) ` x ) ) -> -u z e. RR ) |
86 |
|
fveq2 |
|- ( m = n -> ( F ` m ) = ( F ` n ) ) |
87 |
86
|
fveq1d |
|- ( m = n -> ( ( F ` m ) ` x ) = ( ( F ` n ) ` x ) ) |
88 |
87
|
breq2d |
|- ( m = n -> ( z <_ ( ( F ` m ) ` x ) <-> z <_ ( ( F ` n ) ` x ) ) ) |
89 |
88
|
rspcva |
|- ( ( n e. Z /\ A. m e. Z z <_ ( ( F ` m ) ` x ) ) -> z <_ ( ( F ` n ) ` x ) ) |
90 |
89
|
ancoms |
|- ( ( A. m e. Z z <_ ( ( F ` m ) ` x ) /\ n e. Z ) -> z <_ ( ( F ` n ) ` x ) ) |
91 |
90
|
adantll |
|- ( ( ( ( ( ph /\ x e. D ) /\ z e. RR ) /\ A. m e. Z z <_ ( ( F ` m ) ` x ) ) /\ n e. Z ) -> z <_ ( ( F ` n ) ` x ) ) |
92 |
|
simpllr |
|- ( ( ( ( ( ph /\ x e. D ) /\ z e. RR ) /\ A. m e. Z z <_ ( ( F ` m ) ` x ) ) /\ n e. Z ) -> z e. RR ) |
93 |
25
|
ad4ant14 |
|- ( ( ( ( ( ph /\ x e. D ) /\ z e. RR ) /\ A. m e. Z z <_ ( ( F ` m ) ` x ) ) /\ n e. Z ) -> ( ( F ` n ) ` x ) e. RR ) |
94 |
92 93
|
lenegd |
|- ( ( ( ( ( ph /\ x e. D ) /\ z e. RR ) /\ A. m e. Z z <_ ( ( F ` m ) ` x ) ) /\ n e. Z ) -> ( z <_ ( ( F ` n ) ` x ) <-> -u ( ( F ` n ) ` x ) <_ -u z ) ) |
95 |
91 94
|
mpbid |
|- ( ( ( ( ( ph /\ x e. D ) /\ z e. RR ) /\ A. m e. Z z <_ ( ( F ` m ) ` x ) ) /\ n e. Z ) -> -u ( ( F ` n ) ` x ) <_ -u z ) |
96 |
95
|
ralrimiva |
|- ( ( ( ( ph /\ x e. D ) /\ z e. RR ) /\ A. m e. Z z <_ ( ( F ` m ) ` x ) ) -> A. n e. Z -u ( ( F ` n ) ` x ) <_ -u z ) |
97 |
|
brralrspcev |
|- ( ( -u z e. RR /\ A. n e. Z -u ( ( F ` n ) ` x ) <_ -u z ) -> E. y e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ y ) |
98 |
85 96 97
|
syl2anc |
|- ( ( ( ( ph /\ x e. D ) /\ z e. RR ) /\ A. m e. Z z <_ ( ( F ` m ) ` x ) ) -> E. y e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ y ) |
99 |
98
|
rexlimdva2 |
|- ( ( ph /\ x e. D ) -> ( E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` x ) -> E. y e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ y ) ) |
100 |
83 99
|
mpd |
|- ( ( ph /\ x e. D ) -> E. y e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ y ) |
101 |
8 10 39 100
|
suprclrnmpt |
|- ( ( ph /\ x e. D ) -> sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) e. RR ) |
102 |
5
|
a1i |
|- ( ph -> D = { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) } ) |
103 |
|
nfv |
|- F/ y ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) |
104 |
|
nfv |
|- F/ y E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z |
105 |
|
renegcl |
|- ( y e. RR -> -u y e. RR ) |
106 |
105
|
3ad2ant2 |
|- ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR /\ A. n e. Z y <_ ( ( F ` n ) ` x ) ) -> -u y e. RR ) |
107 |
|
nfv |
|- F/ n ph |
108 |
|
nfcv |
|- F/_ n x |
109 |
|
nfii1 |
|- F/_ n |^|_ n e. Z dom ( F ` n ) |
110 |
108 109
|
nfel |
|- F/ n x e. |^|_ n e. Z dom ( F ` n ) |
111 |
107 110
|
nfan |
|- F/ n ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) |
112 |
62
|
nfel1 |
|- F/ n y e. RR |
113 |
|
nfra1 |
|- F/ n A. n e. Z y <_ ( ( F ` n ) ` x ) |
114 |
111 112 113
|
nf3an |
|- F/ n ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR /\ A. n e. Z y <_ ( ( F ` n ) ` x ) ) |
115 |
|
simpl2 |
|- ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR /\ A. n e. Z y <_ ( ( F ` n ) ` x ) ) /\ n e. Z ) -> y e. RR ) |
116 |
|
simpll |
|- ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ n e. Z ) -> ph ) |
117 |
|
simpr |
|- ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ n e. Z ) -> n e. Z ) |
118 |
22
|
adantll |
|- ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ n e. Z ) -> x e. dom ( F ` n ) ) |
119 |
14
|
3adant3 |
|- ( ( ph /\ n e. Z /\ x e. dom ( F ` n ) ) -> ( F ` n ) : dom ( F ` n ) --> RR ) |
120 |
|
simp3 |
|- ( ( ph /\ n e. Z /\ x e. dom ( F ` n ) ) -> x e. dom ( F ` n ) ) |
121 |
119 120
|
ffvelrnd |
|- ( ( ph /\ n e. Z /\ x e. dom ( F ` n ) ) -> ( ( F ` n ) ` x ) e. RR ) |
122 |
116 117 118 121
|
syl3anc |
|- ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ n e. Z ) -> ( ( F ` n ) ` x ) e. RR ) |
123 |
122
|
3ad2antl1 |
|- ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR /\ A. n e. Z y <_ ( ( F ` n ) ` x ) ) /\ n e. Z ) -> ( ( F ` n ) ` x ) e. RR ) |
124 |
|
rspa |
|- ( ( A. n e. Z y <_ ( ( F ` n ) ` x ) /\ n e. Z ) -> y <_ ( ( F ` n ) ` x ) ) |
125 |
124
|
3ad2antl3 |
|- ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR /\ A. n e. Z y <_ ( ( F ` n ) ` x ) ) /\ n e. Z ) -> y <_ ( ( F ` n ) ` x ) ) |
126 |
|
leneg |
|- ( ( y e. RR /\ ( ( F ` n ) ` x ) e. RR ) -> ( y <_ ( ( F ` n ) ` x ) <-> -u ( ( F ` n ) ` x ) <_ -u y ) ) |
127 |
126
|
biimp3a |
|- ( ( y e. RR /\ ( ( F ` n ) ` x ) e. RR /\ y <_ ( ( F ` n ) ` x ) ) -> -u ( ( F ` n ) ` x ) <_ -u y ) |
128 |
115 123 125 127
|
syl3anc |
|- ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR /\ A. n e. Z y <_ ( ( F ` n ) ` x ) ) /\ n e. Z ) -> -u ( ( F ` n ) ` x ) <_ -u y ) |
129 |
128
|
ex |
|- ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR /\ A. n e. Z y <_ ( ( F ` n ) ` x ) ) -> ( n e. Z -> -u ( ( F ` n ) ` x ) <_ -u y ) ) |
130 |
114 129
|
ralrimi |
|- ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR /\ A. n e. Z y <_ ( ( F ` n ) ` x ) ) -> A. n e. Z -u ( ( F ` n ) ` x ) <_ -u y ) |
131 |
|
brralrspcev |
|- ( ( -u y e. RR /\ A. n e. Z -u ( ( F ` n ) ` x ) <_ -u y ) -> E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z ) |
132 |
106 130 131
|
syl2anc |
|- ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR /\ A. n e. Z y <_ ( ( F ` n ) ` x ) ) -> E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z ) |
133 |
132
|
3exp |
|- ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) -> ( y e. RR -> ( A. n e. Z y <_ ( ( F ` n ) ` x ) -> E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z ) ) ) |
134 |
103 104 133
|
rexlimd |
|- ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) -> ( E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) -> E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z ) ) |
135 |
84
|
3ad2ant2 |
|- ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ z e. RR /\ A. n e. Z -u ( ( F ` n ) ` x ) <_ z ) -> -u z e. RR ) |
136 |
|
nfv |
|- F/ n z e. RR |
137 |
|
nfra1 |
|- F/ n A. n e. Z -u ( ( F ` n ) ` x ) <_ z |
138 |
111 136 137
|
nf3an |
|- F/ n ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ z e. RR /\ A. n e. Z -u ( ( F ` n ) ` x ) <_ z ) |
139 |
122
|
3ad2antl1 |
|- ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ z e. RR /\ A. n e. Z -u ( ( F ` n ) ` x ) <_ z ) /\ n e. Z ) -> ( ( F ` n ) ` x ) e. RR ) |
140 |
|
simpl2 |
|- ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ z e. RR /\ A. n e. Z -u ( ( F ` n ) ` x ) <_ z ) /\ n e. Z ) -> z e. RR ) |
141 |
|
rspa |
|- ( ( A. n e. Z -u ( ( F ` n ) ` x ) <_ z /\ n e. Z ) -> -u ( ( F ` n ) ` x ) <_ z ) |
142 |
141
|
3ad2antl3 |
|- ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ z e. RR /\ A. n e. Z -u ( ( F ` n ) ` x ) <_ z ) /\ n e. Z ) -> -u ( ( F ` n ) ` x ) <_ z ) |
143 |
|
simp3 |
|- ( ( ( ( F ` n ) ` x ) e. RR /\ z e. RR /\ -u ( ( F ` n ) ` x ) <_ z ) -> -u ( ( F ` n ) ` x ) <_ z ) |
144 |
|
renegcl |
|- ( ( ( F ` n ) ` x ) e. RR -> -u ( ( F ` n ) ` x ) e. RR ) |
145 |
144
|
adantr |
|- ( ( ( ( F ` n ) ` x ) e. RR /\ z e. RR ) -> -u ( ( F ` n ) ` x ) e. RR ) |
146 |
|
simpr |
|- ( ( ( ( F ` n ) ` x ) e. RR /\ z e. RR ) -> z e. RR ) |
147 |
|
leneg |
|- ( ( -u ( ( F ` n ) ` x ) e. RR /\ z e. RR ) -> ( -u ( ( F ` n ) ` x ) <_ z <-> -u z <_ -u -u ( ( F ` n ) ` x ) ) ) |
148 |
145 146 147
|
syl2anc |
|- ( ( ( ( F ` n ) ` x ) e. RR /\ z e. RR ) -> ( -u ( ( F ` n ) ` x ) <_ z <-> -u z <_ -u -u ( ( F ` n ) ` x ) ) ) |
149 |
148
|
3adant3 |
|- ( ( ( ( F ` n ) ` x ) e. RR /\ z e. RR /\ -u ( ( F ` n ) ` x ) <_ z ) -> ( -u ( ( F ` n ) ` x ) <_ z <-> -u z <_ -u -u ( ( F ` n ) ` x ) ) ) |
150 |
143 149
|
mpbid |
|- ( ( ( ( F ` n ) ` x ) e. RR /\ z e. RR /\ -u ( ( F ` n ) ` x ) <_ z ) -> -u z <_ -u -u ( ( F ` n ) ` x ) ) |
151 |
|
recn |
|- ( ( ( F ` n ) ` x ) e. RR -> ( ( F ` n ) ` x ) e. CC ) |
152 |
151
|
negnegd |
|- ( ( ( F ` n ) ` x ) e. RR -> -u -u ( ( F ` n ) ` x ) = ( ( F ` n ) ` x ) ) |
153 |
152
|
3ad2ant1 |
|- ( ( ( ( F ` n ) ` x ) e. RR /\ z e. RR /\ -u ( ( F ` n ) ` x ) <_ z ) -> -u -u ( ( F ` n ) ` x ) = ( ( F ` n ) ` x ) ) |
154 |
150 153
|
breqtrd |
|- ( ( ( ( F ` n ) ` x ) e. RR /\ z e. RR /\ -u ( ( F ` n ) ` x ) <_ z ) -> -u z <_ ( ( F ` n ) ` x ) ) |
155 |
139 140 142 154
|
syl3anc |
|- ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ z e. RR /\ A. n e. Z -u ( ( F ` n ) ` x ) <_ z ) /\ n e. Z ) -> -u z <_ ( ( F ` n ) ` x ) ) |
156 |
155
|
ex |
|- ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ z e. RR /\ A. n e. Z -u ( ( F ` n ) ` x ) <_ z ) -> ( n e. Z -> -u z <_ ( ( F ` n ) ` x ) ) ) |
157 |
138 156
|
ralrimi |
|- ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ z e. RR /\ A. n e. Z -u ( ( F ` n ) ` x ) <_ z ) -> A. n e. Z -u z <_ ( ( F ` n ) ` x ) ) |
158 |
|
breq1 |
|- ( y = -u z -> ( y <_ ( ( F ` n ) ` x ) <-> -u z <_ ( ( F ` n ) ` x ) ) ) |
159 |
158
|
ralbidv |
|- ( y = -u z -> ( A. n e. Z y <_ ( ( F ` n ) ` x ) <-> A. n e. Z -u z <_ ( ( F ` n ) ` x ) ) ) |
160 |
159
|
rspcev |
|- ( ( -u z e. RR /\ A. n e. Z -u z <_ ( ( F ` n ) ` x ) ) -> E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) ) |
161 |
135 157 160
|
syl2anc |
|- ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ z e. RR /\ A. n e. Z -u ( ( F ` n ) ` x ) <_ z ) -> E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) ) |
162 |
161
|
3exp |
|- ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) -> ( z e. RR -> ( A. n e. Z -u ( ( F ` n ) ` x ) <_ z -> E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) ) ) ) |
163 |
162
|
rexlimdv |
|- ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) -> ( E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z -> E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) ) ) |
164 |
134 163
|
impbid |
|- ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) -> ( E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) <-> E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z ) ) |
165 |
32 164
|
rabbida |
|- ( ph -> { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) } = { x e. |^|_ n e. Z dom ( F ` n ) | E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z } ) |
166 |
102 165
|
eqtrd |
|- ( ph -> D = { x e. |^|_ n e. Z dom ( F ` n ) | E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z } ) |
167 |
32 166
|
alrimi |
|- ( ph -> A. x D = { x e. |^|_ n e. Z dom ( F ` n ) | E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z } ) |
168 |
|
eqid |
|- sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) = sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) |
169 |
168
|
rgenw |
|- A. x e. D sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) = sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) |
170 |
169
|
a1i |
|- ( ph -> A. x e. D sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) = sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) ) |
171 |
|
mpteq12f |
|- ( ( A. x D = { x e. |^|_ n e. Z dom ( F ` n ) | E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z } /\ A. x e. D sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) = sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) ) -> ( x e. D |-> sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) ) = ( x e. { x e. |^|_ n e. Z dom ( F ` n ) | E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z } |-> sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) ) ) |
172 |
167 170 171
|
syl2anc |
|- ( ph -> ( x e. D |-> sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) ) = ( x e. { x e. |^|_ n e. Z dom ( F ` n ) | E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z } |-> sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) ) ) |
173 |
|
nfv |
|- F/ z ph |
174 |
121
|
renegcld |
|- ( ( ph /\ n e. Z /\ x e. dom ( F ` n ) ) -> -u ( ( F ` n ) ` x ) e. RR ) |
175 |
|
nfv |
|- F/ x ( ph /\ n e. Z ) |
176 |
34
|
a1i |
|- ( ( ph /\ n e. Z ) -> dom ( F ` n ) e. _V ) |
177 |
121
|
3expa |
|- ( ( ( ph /\ n e. Z ) /\ x e. dom ( F ` n ) ) -> ( ( F ` n ) ` x ) e. RR ) |
178 |
14
|
feqmptd |
|- ( ( ph /\ n e. Z ) -> ( F ` n ) = ( x e. dom ( F ` n ) |-> ( ( F ` n ) ` x ) ) ) |
179 |
178
|
eqcomd |
|- ( ( ph /\ n e. Z ) -> ( x e. dom ( F ` n ) |-> ( ( F ` n ) ` x ) ) = ( F ` n ) ) |
180 |
179 12
|
eqeltrd |
|- ( ( ph /\ n e. Z ) -> ( x e. dom ( F ` n ) |-> ( ( F ` n ) ` x ) ) e. ( SMblFn ` S ) ) |
181 |
175 11 176 177 180
|
smfneg |
|- ( ( ph /\ n e. Z ) -> ( x e. dom ( F ` n ) |-> -u ( ( F ` n ) ` x ) ) e. ( SMblFn ` S ) ) |
182 |
|
eqid |
|- { x e. |^|_ n e. Z dom ( F ` n ) | E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z } = { x e. |^|_ n e. Z dom ( F ` n ) | E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z } |
183 |
|
eqid |
|- ( x e. { x e. |^|_ n e. Z dom ( F ` n ) | E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z } |-> sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) ) = ( x e. { x e. |^|_ n e. Z dom ( F ` n ) | E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z } |-> sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) ) |
184 |
107 32 173 1 2 3 174 181 182 183
|
smfsupmpt |
|- ( ph -> ( x e. { x e. |^|_ n e. Z dom ( F ` n ) | E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z } |-> sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) ) e. ( SMblFn ` S ) ) |
185 |
172 184
|
eqeltrd |
|- ( ph -> ( x e. D |-> sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) ) e. ( SMblFn ` S ) ) |
186 |
32 3 38 101 185
|
smfneg |
|- ( ph -> ( x e. D |-> -u sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) ) e. ( SMblFn ` S ) ) |
187 |
31 186
|
eqeltrd |
|- ( ph -> G e. ( SMblFn ` S ) ) |