Step |
Hyp |
Ref |
Expression |
1 |
|
bndth.1 |
|- X = U. J |
2 |
|
bndth.2 |
|- K = ( topGen ` ran (,) ) |
3 |
|
bndth.3 |
|- ( ph -> J e. Comp ) |
4 |
|
bndth.4 |
|- ( ph -> F e. ( J Cn K ) ) |
5 |
|
evth.5 |
|- ( ph -> X =/= (/) ) |
6 |
|
cmptop |
|- ( J e. Comp -> J e. Top ) |
7 |
3 6
|
syl |
|- ( ph -> J e. Top ) |
8 |
1
|
toptopon |
|- ( J e. Top <-> J e. ( TopOn ` X ) ) |
9 |
7 8
|
sylib |
|- ( ph -> J e. ( TopOn ` X ) ) |
10 |
|
uniretop |
|- RR = U. ( topGen ` ran (,) ) |
11 |
2
|
unieqi |
|- U. K = U. ( topGen ` ran (,) ) |
12 |
10 11
|
eqtr4i |
|- RR = U. K |
13 |
1 12
|
cnf |
|- ( F e. ( J Cn K ) -> F : X --> RR ) |
14 |
4 13
|
syl |
|- ( ph -> F : X --> RR ) |
15 |
14
|
feqmptd |
|- ( ph -> F = ( z e. X |-> ( F ` z ) ) ) |
16 |
15 4
|
eqeltrrd |
|- ( ph -> ( z e. X |-> ( F ` z ) ) e. ( J Cn K ) ) |
17 |
|
retopon |
|- ( topGen ` ran (,) ) e. ( TopOn ` RR ) |
18 |
2 17
|
eqeltri |
|- K e. ( TopOn ` RR ) |
19 |
18
|
a1i |
|- ( ph -> K e. ( TopOn ` RR ) ) |
20 |
|
eqid |
|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld ) |
21 |
20
|
cnfldtopon |
|- ( TopOpen ` CCfld ) e. ( TopOn ` CC ) |
22 |
21
|
a1i |
|- ( ph -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) ) |
23 |
|
0cnd |
|- ( ph -> 0 e. CC ) |
24 |
19 22 23
|
cnmptc |
|- ( ph -> ( y e. RR |-> 0 ) e. ( K Cn ( TopOpen ` CCfld ) ) ) |
25 |
20
|
tgioo2 |
|- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR ) |
26 |
2 25
|
eqtri |
|- K = ( ( TopOpen ` CCfld ) |`t RR ) |
27 |
|
ax-resscn |
|- RR C_ CC |
28 |
27
|
a1i |
|- ( ph -> RR C_ CC ) |
29 |
22
|
cnmptid |
|- ( ph -> ( y e. CC |-> y ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) ) |
30 |
26 22 28 29
|
cnmpt1res |
|- ( ph -> ( y e. RR |-> y ) e. ( K Cn ( TopOpen ` CCfld ) ) ) |
31 |
20
|
subcn |
|- - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) |
32 |
31
|
a1i |
|- ( ph -> - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) ) |
33 |
19 24 30 32
|
cnmpt12f |
|- ( ph -> ( y e. RR |-> ( 0 - y ) ) e. ( K Cn ( TopOpen ` CCfld ) ) ) |
34 |
|
df-neg |
|- -u y = ( 0 - y ) |
35 |
|
renegcl |
|- ( y e. RR -> -u y e. RR ) |
36 |
34 35
|
eqeltrrid |
|- ( y e. RR -> ( 0 - y ) e. RR ) |
37 |
36
|
adantl |
|- ( ( ph /\ y e. RR ) -> ( 0 - y ) e. RR ) |
38 |
37
|
fmpttd |
|- ( ph -> ( y e. RR |-> ( 0 - y ) ) : RR --> RR ) |
39 |
38
|
frnd |
|- ( ph -> ran ( y e. RR |-> ( 0 - y ) ) C_ RR ) |
40 |
|
cnrest2 |
|- ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ran ( y e. RR |-> ( 0 - y ) ) C_ RR /\ RR C_ CC ) -> ( ( y e. RR |-> ( 0 - y ) ) e. ( K Cn ( TopOpen ` CCfld ) ) <-> ( y e. RR |-> ( 0 - y ) ) e. ( K Cn ( ( TopOpen ` CCfld ) |`t RR ) ) ) ) |
41 |
22 39 28 40
|
syl3anc |
|- ( ph -> ( ( y e. RR |-> ( 0 - y ) ) e. ( K Cn ( TopOpen ` CCfld ) ) <-> ( y e. RR |-> ( 0 - y ) ) e. ( K Cn ( ( TopOpen ` CCfld ) |`t RR ) ) ) ) |
42 |
33 41
|
mpbid |
|- ( ph -> ( y e. RR |-> ( 0 - y ) ) e. ( K Cn ( ( TopOpen ` CCfld ) |`t RR ) ) ) |
43 |
26
|
oveq2i |
|- ( K Cn K ) = ( K Cn ( ( TopOpen ` CCfld ) |`t RR ) ) |
44 |
42 43
|
eleqtrrdi |
|- ( ph -> ( y e. RR |-> ( 0 - y ) ) e. ( K Cn K ) ) |
45 |
|
negeq |
|- ( y = ( F ` z ) -> -u y = -u ( F ` z ) ) |
46 |
34 45
|
eqtr3id |
|- ( y = ( F ` z ) -> ( 0 - y ) = -u ( F ` z ) ) |
47 |
9 16 19 44 46
|
cnmpt11 |
|- ( ph -> ( z e. X |-> -u ( F ` z ) ) e. ( J Cn K ) ) |
48 |
1 2 3 47 5
|
evth |
|- ( ph -> E. x e. X A. y e. X ( ( z e. X |-> -u ( F ` z ) ) ` y ) <_ ( ( z e. X |-> -u ( F ` z ) ) ` x ) ) |
49 |
|
fveq2 |
|- ( z = y -> ( F ` z ) = ( F ` y ) ) |
50 |
49
|
negeqd |
|- ( z = y -> -u ( F ` z ) = -u ( F ` y ) ) |
51 |
|
eqid |
|- ( z e. X |-> -u ( F ` z ) ) = ( z e. X |-> -u ( F ` z ) ) |
52 |
|
negex |
|- -u ( F ` y ) e. _V |
53 |
50 51 52
|
fvmpt |
|- ( y e. X -> ( ( z e. X |-> -u ( F ` z ) ) ` y ) = -u ( F ` y ) ) |
54 |
53
|
adantl |
|- ( ( ( ph /\ x e. X ) /\ y e. X ) -> ( ( z e. X |-> -u ( F ` z ) ) ` y ) = -u ( F ` y ) ) |
55 |
|
fveq2 |
|- ( z = x -> ( F ` z ) = ( F ` x ) ) |
56 |
55
|
negeqd |
|- ( z = x -> -u ( F ` z ) = -u ( F ` x ) ) |
57 |
|
negex |
|- -u ( F ` x ) e. _V |
58 |
56 51 57
|
fvmpt |
|- ( x e. X -> ( ( z e. X |-> -u ( F ` z ) ) ` x ) = -u ( F ` x ) ) |
59 |
58
|
ad2antlr |
|- ( ( ( ph /\ x e. X ) /\ y e. X ) -> ( ( z e. X |-> -u ( F ` z ) ) ` x ) = -u ( F ` x ) ) |
60 |
54 59
|
breq12d |
|- ( ( ( ph /\ x e. X ) /\ y e. X ) -> ( ( ( z e. X |-> -u ( F ` z ) ) ` y ) <_ ( ( z e. X |-> -u ( F ` z ) ) ` x ) <-> -u ( F ` y ) <_ -u ( F ` x ) ) ) |
61 |
14
|
ffvelrnda |
|- ( ( ph /\ x e. X ) -> ( F ` x ) e. RR ) |
62 |
61
|
adantr |
|- ( ( ( ph /\ x e. X ) /\ y e. X ) -> ( F ` x ) e. RR ) |
63 |
14
|
ffvelrnda |
|- ( ( ph /\ y e. X ) -> ( F ` y ) e. RR ) |
64 |
63
|
adantlr |
|- ( ( ( ph /\ x e. X ) /\ y e. X ) -> ( F ` y ) e. RR ) |
65 |
62 64
|
lenegd |
|- ( ( ( ph /\ x e. X ) /\ y e. X ) -> ( ( F ` x ) <_ ( F ` y ) <-> -u ( F ` y ) <_ -u ( F ` x ) ) ) |
66 |
60 65
|
bitr4d |
|- ( ( ( ph /\ x e. X ) /\ y e. X ) -> ( ( ( z e. X |-> -u ( F ` z ) ) ` y ) <_ ( ( z e. X |-> -u ( F ` z ) ) ` x ) <-> ( F ` x ) <_ ( F ` y ) ) ) |
67 |
66
|
ralbidva |
|- ( ( ph /\ x e. X ) -> ( A. y e. X ( ( z e. X |-> -u ( F ` z ) ) ` y ) <_ ( ( z e. X |-> -u ( F ` z ) ) ` x ) <-> A. y e. X ( F ` x ) <_ ( F ` y ) ) ) |
68 |
67
|
rexbidva |
|- ( ph -> ( E. x e. X A. y e. X ( ( z e. X |-> -u ( F ` z ) ) ` y ) <_ ( ( z e. X |-> -u ( F ` z ) ) ` x ) <-> E. x e. X A. y e. X ( F ` x ) <_ ( F ` y ) ) ) |
69 |
48 68
|
mpbid |
|- ( ph -> E. x e. X A. y e. X ( F ` x ) <_ ( F ` y ) ) |