Step |
Hyp |
Ref |
Expression |
1 |
|
bndth.1 |
⊢ 𝑋 = ∪ 𝐽 |
2 |
|
bndth.2 |
⊢ 𝐾 = ( topGen ‘ ran (,) ) |
3 |
|
bndth.3 |
⊢ ( 𝜑 → 𝐽 ∈ Comp ) |
4 |
|
bndth.4 |
⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) |
5 |
|
evth.5 |
⊢ ( 𝜑 → 𝑋 ≠ ∅ ) |
6 |
|
cmptop |
⊢ ( 𝐽 ∈ Comp → 𝐽 ∈ Top ) |
7 |
3 6
|
syl |
⊢ ( 𝜑 → 𝐽 ∈ Top ) |
8 |
1
|
toptopon |
⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
9 |
7 8
|
sylib |
⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
10 |
|
uniretop |
⊢ ℝ = ∪ ( topGen ‘ ran (,) ) |
11 |
2
|
unieqi |
⊢ ∪ 𝐾 = ∪ ( topGen ‘ ran (,) ) |
12 |
10 11
|
eqtr4i |
⊢ ℝ = ∪ 𝐾 |
13 |
1 12
|
cnf |
⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : 𝑋 ⟶ ℝ ) |
14 |
4 13
|
syl |
⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℝ ) |
15 |
14
|
feqmptd |
⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝑧 ) ) ) |
16 |
15 4
|
eqeltrrd |
⊢ ( 𝜑 → ( 𝑧 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝑧 ) ) ∈ ( 𝐽 Cn 𝐾 ) ) |
17 |
|
retopon |
⊢ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) |
18 |
2 17
|
eqeltri |
⊢ 𝐾 ∈ ( TopOn ‘ ℝ ) |
19 |
18
|
a1i |
⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ ℝ ) ) |
20 |
|
eqid |
⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld ) |
21 |
20
|
cnfldtopon |
⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) |
22 |
21
|
a1i |
⊢ ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ) |
23 |
|
0cnd |
⊢ ( 𝜑 → 0 ∈ ℂ ) |
24 |
19 22 23
|
cnmptc |
⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ 0 ) ∈ ( 𝐾 Cn ( TopOpen ‘ ℂfld ) ) ) |
25 |
20
|
tgioo2 |
⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) |
26 |
2 25
|
eqtri |
⊢ 𝐾 = ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) |
27 |
|
ax-resscn |
⊢ ℝ ⊆ ℂ |
28 |
27
|
a1i |
⊢ ( 𝜑 → ℝ ⊆ ℂ ) |
29 |
22
|
cnmptid |
⊢ ( 𝜑 → ( 𝑦 ∈ ℂ ↦ 𝑦 ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) ) |
30 |
26 22 28 29
|
cnmpt1res |
⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ 𝑦 ) ∈ ( 𝐾 Cn ( TopOpen ‘ ℂfld ) ) ) |
31 |
20
|
subcn |
⊢ − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) |
32 |
31
|
a1i |
⊢ ( 𝜑 → − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) ) |
33 |
19 24 30 32
|
cnmpt12f |
⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ ( 0 − 𝑦 ) ) ∈ ( 𝐾 Cn ( TopOpen ‘ ℂfld ) ) ) |
34 |
|
df-neg |
⊢ - 𝑦 = ( 0 − 𝑦 ) |
35 |
|
renegcl |
⊢ ( 𝑦 ∈ ℝ → - 𝑦 ∈ ℝ ) |
36 |
34 35
|
eqeltrrid |
⊢ ( 𝑦 ∈ ℝ → ( 0 − 𝑦 ) ∈ ℝ ) |
37 |
36
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 0 − 𝑦 ) ∈ ℝ ) |
38 |
37
|
fmpttd |
⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ ( 0 − 𝑦 ) ) : ℝ ⟶ ℝ ) |
39 |
38
|
frnd |
⊢ ( 𝜑 → ran ( 𝑦 ∈ ℝ ↦ ( 0 − 𝑦 ) ) ⊆ ℝ ) |
40 |
|
cnrest2 |
⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ran ( 𝑦 ∈ ℝ ↦ ( 0 − 𝑦 ) ) ⊆ ℝ ∧ ℝ ⊆ ℂ ) → ( ( 𝑦 ∈ ℝ ↦ ( 0 − 𝑦 ) ) ∈ ( 𝐾 Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝑦 ∈ ℝ ↦ ( 0 − 𝑦 ) ) ∈ ( 𝐾 Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) ) |
41 |
22 39 28 40
|
syl3anc |
⊢ ( 𝜑 → ( ( 𝑦 ∈ ℝ ↦ ( 0 − 𝑦 ) ) ∈ ( 𝐾 Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝑦 ∈ ℝ ↦ ( 0 − 𝑦 ) ) ∈ ( 𝐾 Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) ) |
42 |
33 41
|
mpbid |
⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ ( 0 − 𝑦 ) ) ∈ ( 𝐾 Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) |
43 |
26
|
oveq2i |
⊢ ( 𝐾 Cn 𝐾 ) = ( 𝐾 Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) |
44 |
42 43
|
eleqtrrdi |
⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ ( 0 − 𝑦 ) ) ∈ ( 𝐾 Cn 𝐾 ) ) |
45 |
|
negeq |
⊢ ( 𝑦 = ( 𝐹 ‘ 𝑧 ) → - 𝑦 = - ( 𝐹 ‘ 𝑧 ) ) |
46 |
34 45
|
eqtr3id |
⊢ ( 𝑦 = ( 𝐹 ‘ 𝑧 ) → ( 0 − 𝑦 ) = - ( 𝐹 ‘ 𝑧 ) ) |
47 |
9 16 19 44 46
|
cnmpt11 |
⊢ ( 𝜑 → ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ∈ ( 𝐽 Cn 𝐾 ) ) |
48 |
1 2 3 47 5
|
evth |
⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑦 ) ≤ ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) ) |
49 |
|
fveq2 |
⊢ ( 𝑧 = 𝑦 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑦 ) ) |
50 |
49
|
negeqd |
⊢ ( 𝑧 = 𝑦 → - ( 𝐹 ‘ 𝑧 ) = - ( 𝐹 ‘ 𝑦 ) ) |
51 |
|
eqid |
⊢ ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) = ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) |
52 |
|
negex |
⊢ - ( 𝐹 ‘ 𝑦 ) ∈ V |
53 |
50 51 52
|
fvmpt |
⊢ ( 𝑦 ∈ 𝑋 → ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑦 ) = - ( 𝐹 ‘ 𝑦 ) ) |
54 |
53
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑦 ) = - ( 𝐹 ‘ 𝑦 ) ) |
55 |
|
fveq2 |
⊢ ( 𝑧 = 𝑥 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) ) |
56 |
55
|
negeqd |
⊢ ( 𝑧 = 𝑥 → - ( 𝐹 ‘ 𝑧 ) = - ( 𝐹 ‘ 𝑥 ) ) |
57 |
|
negex |
⊢ - ( 𝐹 ‘ 𝑥 ) ∈ V |
58 |
56 51 57
|
fvmpt |
⊢ ( 𝑥 ∈ 𝑋 → ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) = - ( 𝐹 ‘ 𝑥 ) ) |
59 |
58
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) = - ( 𝐹 ‘ 𝑥 ) ) |
60 |
54 59
|
breq12d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑦 ) ≤ ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) ↔ - ( 𝐹 ‘ 𝑦 ) ≤ - ( 𝐹 ‘ 𝑥 ) ) ) |
61 |
14
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ ) |
62 |
61
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ ) |
63 |
14
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ ) |
64 |
63
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ ) |
65 |
62 64
|
lenegd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ↔ - ( 𝐹 ‘ 𝑦 ) ≤ - ( 𝐹 ‘ 𝑥 ) ) ) |
66 |
60 65
|
bitr4d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑦 ) ≤ ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) |
67 |
66
|
ralbidva |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ∀ 𝑦 ∈ 𝑋 ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑦 ) ≤ ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) |
68 |
67
|
rexbidva |
⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑦 ) ≤ ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) |
69 |
48 68
|
mpbid |
⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) |