Step |
Hyp |
Ref |
Expression |
1 |
|
mbfinf.1 |
|- Z = ( ZZ>= ` M ) |
2 |
|
mbfinf.2 |
|- G = ( x e. A |-> inf ( ran ( n e. Z |-> B ) , RR , < ) ) |
3 |
|
mbfinf.3 |
|- ( ph -> M e. ZZ ) |
4 |
|
mbfinf.4 |
|- ( ( ph /\ n e. Z ) -> ( x e. A |-> B ) e. MblFn ) |
5 |
|
mbfinf.5 |
|- ( ( ph /\ ( n e. Z /\ x e. A ) ) -> B e. RR ) |
6 |
|
mbfinf.6 |
|- ( ( ph /\ x e. A ) -> E. y e. RR A. n e. Z y <_ B ) |
7 |
5
|
anass1rs |
|- ( ( ( ph /\ x e. A ) /\ n e. Z ) -> B e. RR ) |
8 |
7
|
fmpttd |
|- ( ( ph /\ x e. A ) -> ( n e. Z |-> B ) : Z --> RR ) |
9 |
8
|
frnd |
|- ( ( ph /\ x e. A ) -> ran ( n e. Z |-> B ) C_ RR ) |
10 |
|
uzid |
|- ( M e. ZZ -> M e. ( ZZ>= ` M ) ) |
11 |
3 10
|
syl |
|- ( ph -> M e. ( ZZ>= ` M ) ) |
12 |
11 1
|
eleqtrrdi |
|- ( ph -> M e. Z ) |
13 |
12
|
adantr |
|- ( ( ph /\ x e. A ) -> M e. Z ) |
14 |
|
eqid |
|- ( n e. Z |-> B ) = ( n e. Z |-> B ) |
15 |
14 7
|
dmmptd |
|- ( ( ph /\ x e. A ) -> dom ( n e. Z |-> B ) = Z ) |
16 |
13 15
|
eleqtrrd |
|- ( ( ph /\ x e. A ) -> M e. dom ( n e. Z |-> B ) ) |
17 |
16
|
ne0d |
|- ( ( ph /\ x e. A ) -> dom ( n e. Z |-> B ) =/= (/) ) |
18 |
|
dm0rn0 |
|- ( dom ( n e. Z |-> B ) = (/) <-> ran ( n e. Z |-> B ) = (/) ) |
19 |
18
|
necon3bii |
|- ( dom ( n e. Z |-> B ) =/= (/) <-> ran ( n e. Z |-> B ) =/= (/) ) |
20 |
17 19
|
sylib |
|- ( ( ph /\ x e. A ) -> ran ( n e. Z |-> B ) =/= (/) ) |
21 |
8
|
ffnd |
|- ( ( ph /\ x e. A ) -> ( n e. Z |-> B ) Fn Z ) |
22 |
|
breq2 |
|- ( z = ( ( n e. Z |-> B ) ` m ) -> ( y <_ z <-> y <_ ( ( n e. Z |-> B ) ` m ) ) ) |
23 |
22
|
ralrn |
|- ( ( n e. Z |-> B ) Fn Z -> ( A. z e. ran ( n e. Z |-> B ) y <_ z <-> A. m e. Z y <_ ( ( n e. Z |-> B ) ` m ) ) ) |
24 |
21 23
|
syl |
|- ( ( ph /\ x e. A ) -> ( A. z e. ran ( n e. Z |-> B ) y <_ z <-> A. m e. Z y <_ ( ( n e. Z |-> B ) ` m ) ) ) |
25 |
|
nfcv |
|- F/_ n y |
26 |
|
nfcv |
|- F/_ n <_ |
27 |
|
nffvmpt1 |
|- F/_ n ( ( n e. Z |-> B ) ` m ) |
28 |
25 26 27
|
nfbr |
|- F/ n y <_ ( ( n e. Z |-> B ) ` m ) |
29 |
|
nfv |
|- F/ m y <_ ( ( n e. Z |-> B ) ` n ) |
30 |
|
fveq2 |
|- ( m = n -> ( ( n e. Z |-> B ) ` m ) = ( ( n e. Z |-> B ) ` n ) ) |
31 |
30
|
breq2d |
|- ( m = n -> ( y <_ ( ( n e. Z |-> B ) ` m ) <-> y <_ ( ( n e. Z |-> B ) ` n ) ) ) |
32 |
28 29 31
|
cbvralw |
|- ( A. m e. Z y <_ ( ( n e. Z |-> B ) ` m ) <-> A. n e. Z y <_ ( ( n e. Z |-> B ) ` n ) ) |
33 |
|
simpr |
|- ( ( ( ph /\ x e. A ) /\ n e. Z ) -> n e. Z ) |
34 |
14
|
fvmpt2 |
|- ( ( n e. Z /\ B e. RR ) -> ( ( n e. Z |-> B ) ` n ) = B ) |
35 |
33 7 34
|
syl2anc |
|- ( ( ( ph /\ x e. A ) /\ n e. Z ) -> ( ( n e. Z |-> B ) ` n ) = B ) |
36 |
35
|
breq2d |
|- ( ( ( ph /\ x e. A ) /\ n e. Z ) -> ( y <_ ( ( n e. Z |-> B ) ` n ) <-> y <_ B ) ) |
37 |
36
|
ralbidva |
|- ( ( ph /\ x e. A ) -> ( A. n e. Z y <_ ( ( n e. Z |-> B ) ` n ) <-> A. n e. Z y <_ B ) ) |
38 |
32 37
|
syl5bb |
|- ( ( ph /\ x e. A ) -> ( A. m e. Z y <_ ( ( n e. Z |-> B ) ` m ) <-> A. n e. Z y <_ B ) ) |
39 |
24 38
|
bitrd |
|- ( ( ph /\ x e. A ) -> ( A. z e. ran ( n e. Z |-> B ) y <_ z <-> A. n e. Z y <_ B ) ) |
40 |
39
|
rexbidv |
|- ( ( ph /\ x e. A ) -> ( E. y e. RR A. z e. ran ( n e. Z |-> B ) y <_ z <-> E. y e. RR A. n e. Z y <_ B ) ) |
41 |
6 40
|
mpbird |
|- ( ( ph /\ x e. A ) -> E. y e. RR A. z e. ran ( n e. Z |-> B ) y <_ z ) |
42 |
|
infrenegsup |
|- ( ( ran ( n e. Z |-> B ) C_ RR /\ ran ( n e. Z |-> B ) =/= (/) /\ E. y e. RR A. z e. ran ( n e. Z |-> B ) y <_ z ) -> inf ( ran ( n e. Z |-> B ) , RR , < ) = -u sup ( { r e. RR | -u r e. ran ( n e. Z |-> B ) } , RR , < ) ) |
43 |
9 20 41 42
|
syl3anc |
|- ( ( ph /\ x e. A ) -> inf ( ran ( n e. Z |-> B ) , RR , < ) = -u sup ( { r e. RR | -u r e. ran ( n e. Z |-> B ) } , RR , < ) ) |
44 |
|
rabid |
|- ( r e. { r e. RR | -u r e. ran ( n e. Z |-> B ) } <-> ( r e. RR /\ -u r e. ran ( n e. Z |-> B ) ) ) |
45 |
7
|
recnd |
|- ( ( ( ph /\ x e. A ) /\ n e. Z ) -> B e. CC ) |
46 |
45
|
adantlr |
|- ( ( ( ( ph /\ x e. A ) /\ r e. RR ) /\ n e. Z ) -> B e. CC ) |
47 |
|
simplr |
|- ( ( ( ( ph /\ x e. A ) /\ r e. RR ) /\ n e. Z ) -> r e. RR ) |
48 |
47
|
recnd |
|- ( ( ( ( ph /\ x e. A ) /\ r e. RR ) /\ n e. Z ) -> r e. CC ) |
49 |
|
negcon2 |
|- ( ( B e. CC /\ r e. CC ) -> ( B = -u r <-> r = -u B ) ) |
50 |
46 48 49
|
syl2anc |
|- ( ( ( ( ph /\ x e. A ) /\ r e. RR ) /\ n e. Z ) -> ( B = -u r <-> r = -u B ) ) |
51 |
|
eqcom |
|- ( r = -u B <-> -u B = r ) |
52 |
50 51
|
bitrdi |
|- ( ( ( ( ph /\ x e. A ) /\ r e. RR ) /\ n e. Z ) -> ( B = -u r <-> -u B = r ) ) |
53 |
35
|
adantlr |
|- ( ( ( ( ph /\ x e. A ) /\ r e. RR ) /\ n e. Z ) -> ( ( n e. Z |-> B ) ` n ) = B ) |
54 |
53
|
eqeq1d |
|- ( ( ( ( ph /\ x e. A ) /\ r e. RR ) /\ n e. Z ) -> ( ( ( n e. Z |-> B ) ` n ) = -u r <-> B = -u r ) ) |
55 |
|
negex |
|- -u B e. _V |
56 |
|
eqid |
|- ( n e. Z |-> -u B ) = ( n e. Z |-> -u B ) |
57 |
56
|
fvmpt2 |
|- ( ( n e. Z /\ -u B e. _V ) -> ( ( n e. Z |-> -u B ) ` n ) = -u B ) |
58 |
55 57
|
mpan2 |
|- ( n e. Z -> ( ( n e. Z |-> -u B ) ` n ) = -u B ) |
59 |
58
|
adantl |
|- ( ( ( ( ph /\ x e. A ) /\ r e. RR ) /\ n e. Z ) -> ( ( n e. Z |-> -u B ) ` n ) = -u B ) |
60 |
59
|
eqeq1d |
|- ( ( ( ( ph /\ x e. A ) /\ r e. RR ) /\ n e. Z ) -> ( ( ( n e. Z |-> -u B ) ` n ) = r <-> -u B = r ) ) |
61 |
52 54 60
|
3bitr4d |
|- ( ( ( ( ph /\ x e. A ) /\ r e. RR ) /\ n e. Z ) -> ( ( ( n e. Z |-> B ) ` n ) = -u r <-> ( ( n e. Z |-> -u B ) ` n ) = r ) ) |
62 |
61
|
ralrimiva |
|- ( ( ( ph /\ x e. A ) /\ r e. RR ) -> A. n e. Z ( ( ( n e. Z |-> B ) ` n ) = -u r <-> ( ( n e. Z |-> -u B ) ` n ) = r ) ) |
63 |
27
|
nfeq1 |
|- F/ n ( ( n e. Z |-> B ) ` m ) = -u r |
64 |
|
nffvmpt1 |
|- F/_ n ( ( n e. Z |-> -u B ) ` m ) |
65 |
64
|
nfeq1 |
|- F/ n ( ( n e. Z |-> -u B ) ` m ) = r |
66 |
63 65
|
nfbi |
|- F/ n ( ( ( n e. Z |-> B ) ` m ) = -u r <-> ( ( n e. Z |-> -u B ) ` m ) = r ) |
67 |
|
nfv |
|- F/ m ( ( ( n e. Z |-> B ) ` n ) = -u r <-> ( ( n e. Z |-> -u B ) ` n ) = r ) |
68 |
|
fveqeq2 |
|- ( m = n -> ( ( ( n e. Z |-> B ) ` m ) = -u r <-> ( ( n e. Z |-> B ) ` n ) = -u r ) ) |
69 |
|
fveqeq2 |
|- ( m = n -> ( ( ( n e. Z |-> -u B ) ` m ) = r <-> ( ( n e. Z |-> -u B ) ` n ) = r ) ) |
70 |
68 69
|
bibi12d |
|- ( m = n -> ( ( ( ( n e. Z |-> B ) ` m ) = -u r <-> ( ( n e. Z |-> -u B ) ` m ) = r ) <-> ( ( ( n e. Z |-> B ) ` n ) = -u r <-> ( ( n e. Z |-> -u B ) ` n ) = r ) ) ) |
71 |
66 67 70
|
cbvralw |
|- ( A. m e. Z ( ( ( n e. Z |-> B ) ` m ) = -u r <-> ( ( n e. Z |-> -u B ) ` m ) = r ) <-> A. n e. Z ( ( ( n e. Z |-> B ) ` n ) = -u r <-> ( ( n e. Z |-> -u B ) ` n ) = r ) ) |
72 |
62 71
|
sylibr |
|- ( ( ( ph /\ x e. A ) /\ r e. RR ) -> A. m e. Z ( ( ( n e. Z |-> B ) ` m ) = -u r <-> ( ( n e. Z |-> -u B ) ` m ) = r ) ) |
73 |
72
|
r19.21bi |
|- ( ( ( ( ph /\ x e. A ) /\ r e. RR ) /\ m e. Z ) -> ( ( ( n e. Z |-> B ) ` m ) = -u r <-> ( ( n e. Z |-> -u B ) ` m ) = r ) ) |
74 |
73
|
rexbidva |
|- ( ( ( ph /\ x e. A ) /\ r e. RR ) -> ( E. m e. Z ( ( n e. Z |-> B ) ` m ) = -u r <-> E. m e. Z ( ( n e. Z |-> -u B ) ` m ) = r ) ) |
75 |
21
|
adantr |
|- ( ( ( ph /\ x e. A ) /\ r e. RR ) -> ( n e. Z |-> B ) Fn Z ) |
76 |
|
fvelrnb |
|- ( ( n e. Z |-> B ) Fn Z -> ( -u r e. ran ( n e. Z |-> B ) <-> E. m e. Z ( ( n e. Z |-> B ) ` m ) = -u r ) ) |
77 |
75 76
|
syl |
|- ( ( ( ph /\ x e. A ) /\ r e. RR ) -> ( -u r e. ran ( n e. Z |-> B ) <-> E. m e. Z ( ( n e. Z |-> B ) ` m ) = -u r ) ) |
78 |
7
|
renegcld |
|- ( ( ( ph /\ x e. A ) /\ n e. Z ) -> -u B e. RR ) |
79 |
78
|
fmpttd |
|- ( ( ph /\ x e. A ) -> ( n e. Z |-> -u B ) : Z --> RR ) |
80 |
79
|
adantr |
|- ( ( ( ph /\ x e. A ) /\ r e. RR ) -> ( n e. Z |-> -u B ) : Z --> RR ) |
81 |
80
|
ffnd |
|- ( ( ( ph /\ x e. A ) /\ r e. RR ) -> ( n e. Z |-> -u B ) Fn Z ) |
82 |
|
fvelrnb |
|- ( ( n e. Z |-> -u B ) Fn Z -> ( r e. ran ( n e. Z |-> -u B ) <-> E. m e. Z ( ( n e. Z |-> -u B ) ` m ) = r ) ) |
83 |
81 82
|
syl |
|- ( ( ( ph /\ x e. A ) /\ r e. RR ) -> ( r e. ran ( n e. Z |-> -u B ) <-> E. m e. Z ( ( n e. Z |-> -u B ) ` m ) = r ) ) |
84 |
74 77 83
|
3bitr4d |
|- ( ( ( ph /\ x e. A ) /\ r e. RR ) -> ( -u r e. ran ( n e. Z |-> B ) <-> r e. ran ( n e. Z |-> -u B ) ) ) |
85 |
84
|
pm5.32da |
|- ( ( ph /\ x e. A ) -> ( ( r e. RR /\ -u r e. ran ( n e. Z |-> B ) ) <-> ( r e. RR /\ r e. ran ( n e. Z |-> -u B ) ) ) ) |
86 |
79
|
frnd |
|- ( ( ph /\ x e. A ) -> ran ( n e. Z |-> -u B ) C_ RR ) |
87 |
86
|
sseld |
|- ( ( ph /\ x e. A ) -> ( r e. ran ( n e. Z |-> -u B ) -> r e. RR ) ) |
88 |
87
|
pm4.71rd |
|- ( ( ph /\ x e. A ) -> ( r e. ran ( n e. Z |-> -u B ) <-> ( r e. RR /\ r e. ran ( n e. Z |-> -u B ) ) ) ) |
89 |
85 88
|
bitr4d |
|- ( ( ph /\ x e. A ) -> ( ( r e. RR /\ -u r e. ran ( n e. Z |-> B ) ) <-> r e. ran ( n e. Z |-> -u B ) ) ) |
90 |
44 89
|
syl5bb |
|- ( ( ph /\ x e. A ) -> ( r e. { r e. RR | -u r e. ran ( n e. Z |-> B ) } <-> r e. ran ( n e. Z |-> -u B ) ) ) |
91 |
90
|
alrimiv |
|- ( ( ph /\ x e. A ) -> A. r ( r e. { r e. RR | -u r e. ran ( n e. Z |-> B ) } <-> r e. ran ( n e. Z |-> -u B ) ) ) |
92 |
|
nfrab1 |
|- F/_ r { r e. RR | -u r e. ran ( n e. Z |-> B ) } |
93 |
|
nfcv |
|- F/_ r ran ( n e. Z |-> -u B ) |
94 |
92 93
|
cleqf |
|- ( { r e. RR | -u r e. ran ( n e. Z |-> B ) } = ran ( n e. Z |-> -u B ) <-> A. r ( r e. { r e. RR | -u r e. ran ( n e. Z |-> B ) } <-> r e. ran ( n e. Z |-> -u B ) ) ) |
95 |
91 94
|
sylibr |
|- ( ( ph /\ x e. A ) -> { r e. RR | -u r e. ran ( n e. Z |-> B ) } = ran ( n e. Z |-> -u B ) ) |
96 |
95
|
supeq1d |
|- ( ( ph /\ x e. A ) -> sup ( { r e. RR | -u r e. ran ( n e. Z |-> B ) } , RR , < ) = sup ( ran ( n e. Z |-> -u B ) , RR , < ) ) |
97 |
96
|
negeqd |
|- ( ( ph /\ x e. A ) -> -u sup ( { r e. RR | -u r e. ran ( n e. Z |-> B ) } , RR , < ) = -u sup ( ran ( n e. Z |-> -u B ) , RR , < ) ) |
98 |
43 97
|
eqtrd |
|- ( ( ph /\ x e. A ) -> inf ( ran ( n e. Z |-> B ) , RR , < ) = -u sup ( ran ( n e. Z |-> -u B ) , RR , < ) ) |
99 |
98
|
mpteq2dva |
|- ( ph -> ( x e. A |-> inf ( ran ( n e. Z |-> B ) , RR , < ) ) = ( x e. A |-> -u sup ( ran ( n e. Z |-> -u B ) , RR , < ) ) ) |
100 |
2 99
|
syl5eq |
|- ( ph -> G = ( x e. A |-> -u sup ( ran ( n e. Z |-> -u B ) , RR , < ) ) ) |
101 |
|
ltso |
|- < Or RR |
102 |
101
|
supex |
|- sup ( ran ( n e. Z |-> -u B ) , RR , < ) e. _V |
103 |
102
|
a1i |
|- ( ( ph /\ x e. A ) -> sup ( ran ( n e. Z |-> -u B ) , RR , < ) e. _V ) |
104 |
|
eqid |
|- ( x e. A |-> sup ( ran ( n e. Z |-> -u B ) , RR , < ) ) = ( x e. A |-> sup ( ran ( n e. Z |-> -u B ) , RR , < ) ) |
105 |
5
|
anassrs |
|- ( ( ( ph /\ n e. Z ) /\ x e. A ) -> B e. RR ) |
106 |
105 4
|
mbfneg |
|- ( ( ph /\ n e. Z ) -> ( x e. A |-> -u B ) e. MblFn ) |
107 |
5
|
renegcld |
|- ( ( ph /\ ( n e. Z /\ x e. A ) ) -> -u B e. RR ) |
108 |
|
renegcl |
|- ( y e. RR -> -u y e. RR ) |
109 |
108
|
ad2antrl |
|- ( ( ( ph /\ x e. A ) /\ ( y e. RR /\ A. n e. Z y <_ B ) ) -> -u y e. RR ) |
110 |
|
simplr |
|- ( ( ( ( ph /\ x e. A ) /\ y e. RR ) /\ n e. Z ) -> y e. RR ) |
111 |
7
|
adantlr |
|- ( ( ( ( ph /\ x e. A ) /\ y e. RR ) /\ n e. Z ) -> B e. RR ) |
112 |
110 111
|
lenegd |
|- ( ( ( ( ph /\ x e. A ) /\ y e. RR ) /\ n e. Z ) -> ( y <_ B <-> -u B <_ -u y ) ) |
113 |
112
|
ralbidva |
|- ( ( ( ph /\ x e. A ) /\ y e. RR ) -> ( A. n e. Z y <_ B <-> A. n e. Z -u B <_ -u y ) ) |
114 |
113
|
biimpd |
|- ( ( ( ph /\ x e. A ) /\ y e. RR ) -> ( A. n e. Z y <_ B -> A. n e. Z -u B <_ -u y ) ) |
115 |
114
|
impr |
|- ( ( ( ph /\ x e. A ) /\ ( y e. RR /\ A. n e. Z y <_ B ) ) -> A. n e. Z -u B <_ -u y ) |
116 |
|
brralrspcev |
|- ( ( -u y e. RR /\ A. n e. Z -u B <_ -u y ) -> E. z e. RR A. n e. Z -u B <_ z ) |
117 |
109 115 116
|
syl2anc |
|- ( ( ( ph /\ x e. A ) /\ ( y e. RR /\ A. n e. Z y <_ B ) ) -> E. z e. RR A. n e. Z -u B <_ z ) |
118 |
6 117
|
rexlimddv |
|- ( ( ph /\ x e. A ) -> E. z e. RR A. n e. Z -u B <_ z ) |
119 |
1 104 3 106 107 118
|
mbfsup |
|- ( ph -> ( x e. A |-> sup ( ran ( n e. Z |-> -u B ) , RR , < ) ) e. MblFn ) |
120 |
103 119
|
mbfneg |
|- ( ph -> ( x e. A |-> -u sup ( ran ( n e. Z |-> -u B ) , RR , < ) ) e. MblFn ) |
121 |
100 120
|
eqeltrd |
|- ( ph -> G e. MblFn ) |