Step | Hyp | Ref
| Expression |
1 | | bndth.1 |
. . 3
⊢ 𝑋 = ∪
𝐽 |
2 | | bndth.2 |
. . 3
⊢ 𝐾 = (topGen‘ran
(,)) |
3 | | bndth.3 |
. . 3
⊢ (𝜑 → 𝐽 ∈ Comp) |
4 | | cmptop 21008 |
. . . . . 6
⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top) |
5 | 3, 4 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ Top) |
6 | 1 | toptopon 20548 |
. . . . 5
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
7 | 5, 6 | sylib 207 |
. . . 4
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
8 | | bndth.4 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) |
9 | | uniretop 22376 |
. . . . . . . . 9
⊢ ℝ =
∪ (topGen‘ran (,)) |
10 | 2 | unieqi 4381 |
. . . . . . . . 9
⊢ ∪ 𝐾 =
∪ (topGen‘ran (,)) |
11 | 9, 10 | eqtr4i 2635 |
. . . . . . . 8
⊢ ℝ =
∪ 𝐾 |
12 | 1, 11 | cnf 20860 |
. . . . . . 7
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶ℝ) |
13 | 8, 12 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹:𝑋⟶ℝ) |
14 | 13 | feqmptd 6159 |
. . . . 5
⊢ (𝜑 → 𝐹 = (𝑧 ∈ 𝑋 ↦ (𝐹‘𝑧))) |
15 | 14, 8 | eqeltrrd 2689 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ 𝑋 ↦ (𝐹‘𝑧)) ∈ (𝐽 Cn 𝐾)) |
16 | | retopon 22377 |
. . . . . 6
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
17 | 2, 16 | eqeltri 2684 |
. . . . 5
⊢ 𝐾 ∈
(TopOn‘ℝ) |
18 | 17 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐾 ∈
(TopOn‘ℝ)) |
19 | | eqid 2610 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
20 | 19 | cnfldtopon 22396 |
. . . . . . . . 9
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
21 | 20 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 →
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ)) |
22 | | 0cnd 9912 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
ℂ) |
23 | 18, 21, 22 | cnmptc 21275 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ 0) ∈ (𝐾 Cn
(TopOpen‘ℂfld))) |
24 | 19 | tgioo2 22414 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
25 | 2, 24 | eqtri 2632 |
. . . . . . . 8
⊢ 𝐾 =
((TopOpen‘ℂfld) ↾t
ℝ) |
26 | | ax-resscn 9872 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
27 | 26 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℝ ⊆
ℂ) |
28 | 21 | cnmptid 21274 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ ℂ ↦ 𝑦) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
29 | 25, 21, 27, 28 | cnmpt1res 21289 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ 𝑦) ∈ (𝐾 Cn
(TopOpen‘ℂfld))) |
30 | 19 | subcn 22477 |
. . . . . . . 8
⊢ −
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
31 | 30 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → − ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) |
32 | 18, 23, 29, 31 | cnmpt12f 21279 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (0 − 𝑦)) ∈ (𝐾 Cn
(TopOpen‘ℂfld))) |
33 | | df-neg 10148 |
. . . . . . . . . . 11
⊢ -𝑦 = (0 − 𝑦) |
34 | | renegcl 10223 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ → -𝑦 ∈
ℝ) |
35 | 33, 34 | syl5eqelr 2693 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ → (0
− 𝑦) ∈
ℝ) |
36 | 35 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (0 − 𝑦) ∈
ℝ) |
37 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ ↦ (0
− 𝑦)) = (𝑦 ∈ ℝ ↦ (0
− 𝑦)) |
38 | 36, 37 | fmptd 6292 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (0 − 𝑦)):ℝ⟶ℝ) |
39 | | frn 5966 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℝ ↦ (0
− 𝑦)):ℝ⟶ℝ → ran (𝑦 ∈ ℝ ↦ (0
− 𝑦)) ⊆
ℝ) |
40 | 38, 39 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ran (𝑦 ∈ ℝ ↦ (0 − 𝑦)) ⊆
ℝ) |
41 | | cnrest2 20900 |
. . . . . . 7
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ ran (𝑦 ∈ ℝ
↦ (0 − 𝑦))
⊆ ℝ ∧ ℝ ⊆ ℂ) → ((𝑦 ∈ ℝ ↦ (0 − 𝑦)) ∈ (𝐾 Cn (TopOpen‘ℂfld))
↔ (𝑦 ∈ ℝ
↦ (0 − 𝑦))
∈ (𝐾 Cn
((TopOpen‘ℂfld) ↾t
ℝ)))) |
42 | 21, 40, 27, 41 | syl3anc 1318 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ (0 − 𝑦)) ∈ (𝐾 Cn (TopOpen‘ℂfld))
↔ (𝑦 ∈ ℝ
↦ (0 − 𝑦))
∈ (𝐾 Cn
((TopOpen‘ℂfld) ↾t
ℝ)))) |
43 | 32, 42 | mpbid 221 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (0 − 𝑦)) ∈ (𝐾 Cn ((TopOpen‘ℂfld)
↾t ℝ))) |
44 | 25 | oveq2i 6560 |
. . . . 5
⊢ (𝐾 Cn 𝐾) = (𝐾 Cn ((TopOpen‘ℂfld)
↾t ℝ)) |
45 | 43, 44 | syl6eleqr 2699 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (0 − 𝑦)) ∈ (𝐾 Cn 𝐾)) |
46 | | negeq 10152 |
. . . . 5
⊢ (𝑦 = (𝐹‘𝑧) → -𝑦 = -(𝐹‘𝑧)) |
47 | 33, 46 | syl5eqr 2658 |
. . . 4
⊢ (𝑦 = (𝐹‘𝑧) → (0 − 𝑦) = -(𝐹‘𝑧)) |
48 | 7, 15, 18, 45, 47 | cnmpt11 21276 |
. . 3
⊢ (𝜑 → (𝑧 ∈ 𝑋 ↦ -(𝐹‘𝑧)) ∈ (𝐽 Cn 𝐾)) |
49 | | evth.5 |
. . 3
⊢ (𝜑 → 𝑋 ≠ ∅) |
50 | 1, 2, 3, 48, 49 | evth 22566 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑧 ∈ 𝑋 ↦ -(𝐹‘𝑧))‘𝑦) ≤ ((𝑧 ∈ 𝑋 ↦ -(𝐹‘𝑧))‘𝑥)) |
51 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑧 = 𝑦 → (𝐹‘𝑧) = (𝐹‘𝑦)) |
52 | 51 | negeqd 10154 |
. . . . . . . 8
⊢ (𝑧 = 𝑦 → -(𝐹‘𝑧) = -(𝐹‘𝑦)) |
53 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝑋 ↦ -(𝐹‘𝑧)) = (𝑧 ∈ 𝑋 ↦ -(𝐹‘𝑧)) |
54 | | negex 10158 |
. . . . . . . 8
⊢ -(𝐹‘𝑦) ∈ V |
55 | 52, 53, 54 | fvmpt 6191 |
. . . . . . 7
⊢ (𝑦 ∈ 𝑋 → ((𝑧 ∈ 𝑋 ↦ -(𝐹‘𝑧))‘𝑦) = -(𝐹‘𝑦)) |
56 | 55 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝑧 ∈ 𝑋 ↦ -(𝐹‘𝑧))‘𝑦) = -(𝐹‘𝑦)) |
57 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑧 = 𝑥 → (𝐹‘𝑧) = (𝐹‘𝑥)) |
58 | 57 | negeqd 10154 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → -(𝐹‘𝑧) = -(𝐹‘𝑥)) |
59 | | negex 10158 |
. . . . . . . 8
⊢ -(𝐹‘𝑥) ∈ V |
60 | 58, 53, 59 | fvmpt 6191 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑋 → ((𝑧 ∈ 𝑋 ↦ -(𝐹‘𝑧))‘𝑥) = -(𝐹‘𝑥)) |
61 | 60 | ad2antlr 759 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝑧 ∈ 𝑋 ↦ -(𝐹‘𝑧))‘𝑥) = -(𝐹‘𝑥)) |
62 | 56, 61 | breq12d 4596 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (((𝑧 ∈ 𝑋 ↦ -(𝐹‘𝑧))‘𝑦) ≤ ((𝑧 ∈ 𝑋 ↦ -(𝐹‘𝑧))‘𝑥) ↔ -(𝐹‘𝑦) ≤ -(𝐹‘𝑥))) |
63 | 13 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ ℝ) |
64 | 63 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝐹‘𝑥) ∈ ℝ) |
65 | 13 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐹‘𝑦) ∈ ℝ) |
66 | 65 | adantlr 747 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝐹‘𝑦) ∈ ℝ) |
67 | 64, 66 | lenegd 10485 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑥) ≤ (𝐹‘𝑦) ↔ -(𝐹‘𝑦) ≤ -(𝐹‘𝑥))) |
68 | 62, 67 | bitr4d 270 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (((𝑧 ∈ 𝑋 ↦ -(𝐹‘𝑧))‘𝑦) ≤ ((𝑧 ∈ 𝑋 ↦ -(𝐹‘𝑧))‘𝑥) ↔ (𝐹‘𝑥) ≤ (𝐹‘𝑦))) |
69 | 68 | ralbidva 2968 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (∀𝑦 ∈ 𝑋 ((𝑧 ∈ 𝑋 ↦ -(𝐹‘𝑧))‘𝑦) ≤ ((𝑧 ∈ 𝑋 ↦ -(𝐹‘𝑧))‘𝑥) ↔ ∀𝑦 ∈ 𝑋 (𝐹‘𝑥) ≤ (𝐹‘𝑦))) |
70 | 69 | rexbidva 3031 |
. 2
⊢ (𝜑 → (∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑧 ∈ 𝑋 ↦ -(𝐹‘𝑧))‘𝑦) ≤ ((𝑧 ∈ 𝑋 ↦ -(𝐹‘𝑧))‘𝑥) ↔ ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘𝑥) ≤ (𝐹‘𝑦))) |
71 | 50, 70 | mpbid 221 |
1
⊢ (𝜑 → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘𝑥) ≤ (𝐹‘𝑦)) |