Step |
Hyp |
Ref |
Expression |
1 |
|
cncmpmax.1 |
|- T = U. J |
2 |
|
cncmpmax.2 |
|- K = ( topGen ` ran (,) ) |
3 |
|
cncmpmax.3 |
|- ( ph -> J e. Comp ) |
4 |
|
cncmpmax.4 |
|- ( ph -> F e. ( J Cn K ) ) |
5 |
|
cncmpmax.5 |
|- ( ph -> T =/= (/) ) |
6 |
1 2 3 4 5
|
evth |
|- ( ph -> E. x e. T A. t e. T ( F ` t ) <_ ( F ` x ) ) |
7 |
|
eqid |
|- ( J Cn K ) = ( J Cn K ) |
8 |
2 1 7 4
|
fcnre |
|- ( ph -> F : T --> RR ) |
9 |
8
|
frnd |
|- ( ph -> ran F C_ RR ) |
10 |
9
|
adantr |
|- ( ( ph /\ ( x e. T /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) ) -> ran F C_ RR ) |
11 |
8
|
ffund |
|- ( ph -> Fun F ) |
12 |
11
|
adantr |
|- ( ( ph /\ x e. T ) -> Fun F ) |
13 |
|
simpr |
|- ( ( ph /\ x e. T ) -> x e. T ) |
14 |
8
|
adantr |
|- ( ( ph /\ x e. T ) -> F : T --> RR ) |
15 |
14
|
fdmd |
|- ( ( ph /\ x e. T ) -> dom F = T ) |
16 |
13 15
|
eleqtrrd |
|- ( ( ph /\ x e. T ) -> x e. dom F ) |
17 |
|
fvelrn |
|- ( ( Fun F /\ x e. dom F ) -> ( F ` x ) e. ran F ) |
18 |
12 16 17
|
syl2anc |
|- ( ( ph /\ x e. T ) -> ( F ` x ) e. ran F ) |
19 |
18
|
adantrr |
|- ( ( ph /\ ( x e. T /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) ) -> ( F ` x ) e. ran F ) |
20 |
|
ffn |
|- ( F : T --> RR -> F Fn T ) |
21 |
|
fvelrnb |
|- ( F Fn T -> ( y e. ran F <-> E. s e. T ( F ` s ) = y ) ) |
22 |
8 20 21
|
3syl |
|- ( ph -> ( y e. ran F <-> E. s e. T ( F ` s ) = y ) ) |
23 |
22
|
biimpa |
|- ( ( ph /\ y e. ran F ) -> E. s e. T ( F ` s ) = y ) |
24 |
|
df-rex |
|- ( E. s e. T ( F ` s ) = y <-> E. s ( s e. T /\ ( F ` s ) = y ) ) |
25 |
23 24
|
sylib |
|- ( ( ph /\ y e. ran F ) -> E. s ( s e. T /\ ( F ` s ) = y ) ) |
26 |
25
|
adantlr |
|- ( ( ( ph /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) /\ y e. ran F ) -> E. s ( s e. T /\ ( F ` s ) = y ) ) |
27 |
|
simprr |
|- ( ( ( ( ph /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) /\ y e. ran F ) /\ ( s e. T /\ ( F ` s ) = y ) ) -> ( F ` s ) = y ) |
28 |
|
simpllr |
|- ( ( ( ( ph /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) /\ y e. ran F ) /\ ( s e. T /\ ( F ` s ) = y ) ) -> A. t e. T ( F ` t ) <_ ( F ` x ) ) |
29 |
|
simprl |
|- ( ( ( ( ph /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) /\ y e. ran F ) /\ ( s e. T /\ ( F ` s ) = y ) ) -> s e. T ) |
30 |
|
fveq2 |
|- ( t = s -> ( F ` t ) = ( F ` s ) ) |
31 |
30
|
breq1d |
|- ( t = s -> ( ( F ` t ) <_ ( F ` x ) <-> ( F ` s ) <_ ( F ` x ) ) ) |
32 |
31
|
rspccva |
|- ( ( A. t e. T ( F ` t ) <_ ( F ` x ) /\ s e. T ) -> ( F ` s ) <_ ( F ` x ) ) |
33 |
28 29 32
|
syl2anc |
|- ( ( ( ( ph /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) /\ y e. ran F ) /\ ( s e. T /\ ( F ` s ) = y ) ) -> ( F ` s ) <_ ( F ` x ) ) |
34 |
27 33
|
eqbrtrrd |
|- ( ( ( ( ph /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) /\ y e. ran F ) /\ ( s e. T /\ ( F ` s ) = y ) ) -> y <_ ( F ` x ) ) |
35 |
26 34
|
exlimddv |
|- ( ( ( ph /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) /\ y e. ran F ) -> y <_ ( F ` x ) ) |
36 |
35
|
ralrimiva |
|- ( ( ph /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) -> A. y e. ran F y <_ ( F ` x ) ) |
37 |
36
|
adantrl |
|- ( ( ph /\ ( x e. T /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) ) -> A. y e. ran F y <_ ( F ` x ) ) |
38 |
|
ubelsupr |
|- ( ( ran F C_ RR /\ ( F ` x ) e. ran F /\ A. y e. ran F y <_ ( F ` x ) ) -> ( F ` x ) = sup ( ran F , RR , < ) ) |
39 |
10 19 37 38
|
syl3anc |
|- ( ( ph /\ ( x e. T /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) ) -> ( F ` x ) = sup ( ran F , RR , < ) ) |
40 |
39
|
eqcomd |
|- ( ( ph /\ ( x e. T /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) ) -> sup ( ran F , RR , < ) = ( F ` x ) ) |
41 |
40 19
|
eqeltrd |
|- ( ( ph /\ ( x e. T /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) ) -> sup ( ran F , RR , < ) e. ran F ) |
42 |
10 41
|
sseldd |
|- ( ( ph /\ ( x e. T /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) ) -> sup ( ran F , RR , < ) e. RR ) |
43 |
|
simplrr |
|- ( ( ( ph /\ ( x e. T /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) ) /\ s e. T ) -> A. t e. T ( F ` t ) <_ ( F ` x ) ) |
44 |
43 32
|
sylancom |
|- ( ( ( ph /\ ( x e. T /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) ) /\ s e. T ) -> ( F ` s ) <_ ( F ` x ) ) |
45 |
40
|
adantr |
|- ( ( ( ph /\ ( x e. T /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) ) /\ s e. T ) -> sup ( ran F , RR , < ) = ( F ` x ) ) |
46 |
44 45
|
breqtrrd |
|- ( ( ( ph /\ ( x e. T /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) ) /\ s e. T ) -> ( F ` s ) <_ sup ( ran F , RR , < ) ) |
47 |
46
|
ralrimiva |
|- ( ( ph /\ ( x e. T /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) ) -> A. s e. T ( F ` s ) <_ sup ( ran F , RR , < ) ) |
48 |
30
|
breq1d |
|- ( t = s -> ( ( F ` t ) <_ sup ( ran F , RR , < ) <-> ( F ` s ) <_ sup ( ran F , RR , < ) ) ) |
49 |
48
|
cbvralvw |
|- ( A. t e. T ( F ` t ) <_ sup ( ran F , RR , < ) <-> A. s e. T ( F ` s ) <_ sup ( ran F , RR , < ) ) |
50 |
47 49
|
sylibr |
|- ( ( ph /\ ( x e. T /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) ) -> A. t e. T ( F ` t ) <_ sup ( ran F , RR , < ) ) |
51 |
41 42 50
|
3jca |
|- ( ( ph /\ ( x e. T /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) ) -> ( sup ( ran F , RR , < ) e. ran F /\ sup ( ran F , RR , < ) e. RR /\ A. t e. T ( F ` t ) <_ sup ( ran F , RR , < ) ) ) |
52 |
6 51
|
rexlimddv |
|- ( ph -> ( sup ( ran F , RR , < ) e. ran F /\ sup ( ran F , RR , < ) e. RR /\ A. t e. T ( F ` t ) <_ sup ( ran F , RR , < ) ) ) |