Step | Hyp | Ref
| Expression |
1 | | p0ex 4853 |
. . . . . 6
⊢ {∅}
∈ V |
2 | 1 | prid2 4298 |
. . . . 5
⊢ {∅}
∈ {∅, {∅}} |
3 | 2 | a1i 11 |
. . . 4
⊢ (𝑋 = ∅ → {∅}
∈ {∅, {∅}}) |
4 | | ixpeq1 7919 |
. . . . . 6
⊢ (𝑋 = ∅ → X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) = X𝑖 ∈ ∅ ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
5 | | ixp0x 7936 |
. . . . . . 7
⊢ X𝑖 ∈
∅ ((𝐴‘𝑖)(,)(𝐵‘𝑖)) = {∅} |
6 | 5 | a1i 11 |
. . . . . 6
⊢ (𝑋 = ∅ → X𝑖 ∈
∅ ((𝐴‘𝑖)(,)(𝐵‘𝑖)) = {∅}) |
7 | 4, 6 | eqtrd 2656 |
. . . . 5
⊢ (𝑋 = ∅ → X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) = {∅}) |
8 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑋 = ∅ →
(ℝ^‘𝑋) =
(ℝ^‘∅)) |
9 | 8 | fveq2d 6195 |
. . . . . 6
⊢ (𝑋 = ∅ →
(TopOpen‘(ℝ^‘𝑋)) =
(TopOpen‘(ℝ^‘∅))) |
10 | | rrxtopn0b 40516 |
. . . . . . 7
⊢
(TopOpen‘(ℝ^‘∅)) = {∅,
{∅}} |
11 | 10 | a1i 11 |
. . . . . 6
⊢ (𝑋 = ∅ →
(TopOpen‘(ℝ^‘∅)) = {∅,
{∅}}) |
12 | 9, 11 | eqtrd 2656 |
. . . . 5
⊢ (𝑋 = ∅ →
(TopOpen‘(ℝ^‘𝑋)) = {∅, {∅}}) |
13 | 7, 12 | eleq12d 2695 |
. . . 4
⊢ (𝑋 = ∅ → (X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∈
(TopOpen‘(ℝ^‘𝑋)) ↔ {∅} ∈ {∅,
{∅}})) |
14 | 3, 13 | mpbird 247 |
. . 3
⊢ (𝑋 = ∅ → X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∈
(TopOpen‘(ℝ^‘𝑋))) |
15 | 14 | adantl 482 |
. 2
⊢ ((𝜑 ∧ 𝑋 = ∅) → X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∈
(TopOpen‘(ℝ^‘𝑋))) |
16 | | neqne 2802 |
. . . 4
⊢ (¬
𝑋 = ∅ → 𝑋 ≠ ∅) |
17 | 16 | adantl 482 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝑋 ≠ ∅) |
18 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑗 → (𝐴‘𝑖) = (𝐴‘𝑗)) |
19 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑗 → (𝐵‘𝑖) = (𝐵‘𝑗)) |
20 | 18, 19 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑗 → ((𝐴‘𝑖)(,)(𝐵‘𝑖)) = ((𝐴‘𝑗)(,)(𝐵‘𝑗))) |
21 | 20 | cbvixpv 7926 |
. . . . . . . . 9
⊢ X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) = X𝑗 ∈ 𝑋 ((𝐴‘𝑗)(,)(𝐵‘𝑗)) |
22 | 21 | eleq2i 2693 |
. . . . . . . 8
⊢ (𝑓 ∈ X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ↔ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐴‘𝑗)(,)(𝐵‘𝑗))) |
23 | 22 | biimpi 206 |
. . . . . . 7
⊢ (𝑓 ∈ X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) → 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐴‘𝑗)(,)(𝐵‘𝑗))) |
24 | 23 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) → 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐴‘𝑗)(,)(𝐵‘𝑗))) |
25 | | ioorrnopn.x |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ Fin) |
26 | 25 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) → 𝑋 ∈ Fin) |
27 | 22, 26 | sylan2br 493 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐴‘𝑗)(,)(𝐵‘𝑗))) → 𝑋 ∈ Fin) |
28 | | simplr 792 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) → 𝑋 ≠ ∅) |
29 | 22, 28 | sylan2br 493 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐴‘𝑗)(,)(𝐵‘𝑗))) → 𝑋 ≠ ∅) |
30 | | ioorrnopn.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴:𝑋⟶ℝ) |
31 | 30 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) → 𝐴:𝑋⟶ℝ) |
32 | 22, 31 | sylan2br 493 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐴‘𝑗)(,)(𝐵‘𝑗))) → 𝐴:𝑋⟶ℝ) |
33 | | ioorrnopn.b |
. . . . . . . . 9
⊢ (𝜑 → 𝐵:𝑋⟶ℝ) |
34 | 33 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) → 𝐵:𝑋⟶ℝ) |
35 | 22, 34 | sylan2br 493 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐴‘𝑗)(,)(𝐵‘𝑗))) → 𝐵:𝑋⟶ℝ) |
36 | | simpr 477 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) → 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
37 | 22, 36 | sylan2br 493 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐴‘𝑗)(,)(𝐵‘𝑗))) → 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
38 | | eqid 2622 |
. . . . . . 7
⊢ ran
(𝑖 ∈ 𝑋 ↦ if(((𝐵‘𝑖) − (𝑓‘𝑖)) ≤ ((𝑓‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝑓‘𝑖)), ((𝑓‘𝑖) − (𝐴‘𝑖)))) = ran (𝑖 ∈ 𝑋 ↦ if(((𝐵‘𝑖) − (𝑓‘𝑖)) ≤ ((𝑓‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝑓‘𝑖)), ((𝑓‘𝑖) − (𝐴‘𝑖)))) |
39 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑖 → (𝐵‘𝑗) = (𝐵‘𝑖)) |
40 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑖 → (𝑓‘𝑗) = (𝑓‘𝑖)) |
41 | 39, 40 | oveq12d 6668 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑖 → ((𝐵‘𝑗) − (𝑓‘𝑗)) = ((𝐵‘𝑖) − (𝑓‘𝑖))) |
42 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑖 → (𝐴‘𝑗) = (𝐴‘𝑖)) |
43 | 40, 42 | oveq12d 6668 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑖 → ((𝑓‘𝑗) − (𝐴‘𝑗)) = ((𝑓‘𝑖) − (𝐴‘𝑖))) |
44 | 41, 43 | breq12d 4666 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑖 → (((𝐵‘𝑗) − (𝑓‘𝑗)) ≤ ((𝑓‘𝑗) − (𝐴‘𝑗)) ↔ ((𝐵‘𝑖) − (𝑓‘𝑖)) ≤ ((𝑓‘𝑖) − (𝐴‘𝑖)))) |
45 | 44, 41, 43 | ifbieq12d 4113 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑖 → if(((𝐵‘𝑗) − (𝑓‘𝑗)) ≤ ((𝑓‘𝑗) − (𝐴‘𝑗)), ((𝐵‘𝑗) − (𝑓‘𝑗)), ((𝑓‘𝑗) − (𝐴‘𝑗))) = if(((𝐵‘𝑖) − (𝑓‘𝑖)) ≤ ((𝑓‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝑓‘𝑖)), ((𝑓‘𝑖) − (𝐴‘𝑖)))) |
46 | 45 | cbvmptv 4750 |
. . . . . . . . 9
⊢ (𝑗 ∈ 𝑋 ↦ if(((𝐵‘𝑗) − (𝑓‘𝑗)) ≤ ((𝑓‘𝑗) − (𝐴‘𝑗)), ((𝐵‘𝑗) − (𝑓‘𝑗)), ((𝑓‘𝑗) − (𝐴‘𝑗)))) = (𝑖 ∈ 𝑋 ↦ if(((𝐵‘𝑖) − (𝑓‘𝑖)) ≤ ((𝑓‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝑓‘𝑖)), ((𝑓‘𝑖) − (𝐴‘𝑖)))) |
47 | 46 | rneqi 5352 |
. . . . . . . 8
⊢ ran
(𝑗 ∈ 𝑋 ↦ if(((𝐵‘𝑗) − (𝑓‘𝑗)) ≤ ((𝑓‘𝑗) − (𝐴‘𝑗)), ((𝐵‘𝑗) − (𝑓‘𝑗)), ((𝑓‘𝑗) − (𝐴‘𝑗)))) = ran (𝑖 ∈ 𝑋 ↦ if(((𝐵‘𝑖) − (𝑓‘𝑖)) ≤ ((𝑓‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝑓‘𝑖)), ((𝑓‘𝑖) − (𝐴‘𝑖)))) |
48 | 47 | infeq1i 8384 |
. . . . . . 7
⊢ inf(ran
(𝑗 ∈ 𝑋 ↦ if(((𝐵‘𝑗) − (𝑓‘𝑗)) ≤ ((𝑓‘𝑗) − (𝐴‘𝑗)), ((𝐵‘𝑗) − (𝑓‘𝑗)), ((𝑓‘𝑗) − (𝐴‘𝑗)))), ℝ, < ) = inf(ran (𝑖 ∈ 𝑋 ↦ if(((𝐵‘𝑖) − (𝑓‘𝑖)) ≤ ((𝑓‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝑓‘𝑖)), ((𝑓‘𝑖) − (𝐴‘𝑖)))), ℝ, < ) |
49 | | eqid 2622 |
. . . . . . 7
⊢ (𝑓(ball‘(𝑎 ∈ (ℝ ↑𝑚
𝑋), 𝑏 ∈ (ℝ ↑𝑚
𝑋) ↦
(√‘Σ𝑘
∈ 𝑋 (((𝑎‘𝑘) − (𝑏‘𝑘))↑2))))inf(ran (𝑗 ∈ 𝑋 ↦ if(((𝐵‘𝑗) − (𝑓‘𝑗)) ≤ ((𝑓‘𝑗) − (𝐴‘𝑗)), ((𝐵‘𝑗) − (𝑓‘𝑗)), ((𝑓‘𝑗) − (𝐴‘𝑗)))), ℝ, < )) = (𝑓(ball‘(𝑎 ∈ (ℝ ↑𝑚
𝑋), 𝑏 ∈ (ℝ ↑𝑚
𝑋) ↦
(√‘Σ𝑘
∈ 𝑋 (((𝑎‘𝑘) − (𝑏‘𝑘))↑2))))inf(ran (𝑗 ∈ 𝑋 ↦ if(((𝐵‘𝑗) − (𝑓‘𝑗)) ≤ ((𝑓‘𝑗) − (𝐴‘𝑗)), ((𝐵‘𝑗) − (𝑓‘𝑗)), ((𝑓‘𝑗) − (𝐴‘𝑗)))), ℝ, < )) |
50 | | fveq1 6190 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑔 → (𝑎‘𝑘) = (𝑔‘𝑘)) |
51 | 50 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑔 → ((𝑎‘𝑘) − (𝑏‘𝑘)) = ((𝑔‘𝑘) − (𝑏‘𝑘))) |
52 | 51 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑔 → (((𝑎‘𝑘) − (𝑏‘𝑘))↑2) = (((𝑔‘𝑘) − (𝑏‘𝑘))↑2)) |
53 | 52 | sumeq2ad 14434 |
. . . . . . . . 9
⊢ (𝑎 = 𝑔 → Σ𝑘 ∈ 𝑋 (((𝑎‘𝑘) − (𝑏‘𝑘))↑2) = Σ𝑘 ∈ 𝑋 (((𝑔‘𝑘) − (𝑏‘𝑘))↑2)) |
54 | 53 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑎 = 𝑔 → (√‘Σ𝑘 ∈ 𝑋 (((𝑎‘𝑘) − (𝑏‘𝑘))↑2)) = (√‘Σ𝑘 ∈ 𝑋 (((𝑔‘𝑘) − (𝑏‘𝑘))↑2))) |
55 | | fveq1 6190 |
. . . . . . . . . . . 12
⊢ (𝑏 = ℎ → (𝑏‘𝑘) = (ℎ‘𝑘)) |
56 | 55 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝑏 = ℎ → ((𝑔‘𝑘) − (𝑏‘𝑘)) = ((𝑔‘𝑘) − (ℎ‘𝑘))) |
57 | 56 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝑏 = ℎ → (((𝑔‘𝑘) − (𝑏‘𝑘))↑2) = (((𝑔‘𝑘) − (ℎ‘𝑘))↑2)) |
58 | 57 | sumeq2ad 14434 |
. . . . . . . . 9
⊢ (𝑏 = ℎ → Σ𝑘 ∈ 𝑋 (((𝑔‘𝑘) − (𝑏‘𝑘))↑2) = Σ𝑘 ∈ 𝑋 (((𝑔‘𝑘) − (ℎ‘𝑘))↑2)) |
59 | 58 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑏 = ℎ → (√‘Σ𝑘 ∈ 𝑋 (((𝑔‘𝑘) − (𝑏‘𝑘))↑2)) = (√‘Σ𝑘 ∈ 𝑋 (((𝑔‘𝑘) − (ℎ‘𝑘))↑2))) |
60 | 54, 59 | cbvmpt2v 6735 |
. . . . . . 7
⊢ (𝑎 ∈ (ℝ
↑𝑚 𝑋), 𝑏 ∈ (ℝ ↑𝑚
𝑋) ↦
(√‘Σ𝑘
∈ 𝑋 (((𝑎‘𝑘) − (𝑏‘𝑘))↑2))) = (𝑔 ∈ (ℝ ↑𝑚
𝑋), ℎ ∈ (ℝ ↑𝑚
𝑋) ↦
(√‘Σ𝑘
∈ 𝑋 (((𝑔‘𝑘) − (ℎ‘𝑘))↑2))) |
61 | 27, 29, 32, 35, 37, 38, 48, 49, 60 | ioorrnopnlem 40524 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐴‘𝑗)(,)(𝐵‘𝑗))) → ∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝑓 ∈ 𝑣 ∧ 𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) |
62 | 24, 61 | syldan 487 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) → ∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝑓 ∈ 𝑣 ∧ 𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) |
63 | 62 | ralrimiva 2966 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ∀𝑓 ∈ X
𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝑓 ∈ 𝑣 ∧ 𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) |
64 | | eqid 2622 |
. . . . . . . 8
⊢
(TopOpen‘(ℝ^‘𝑋)) = (TopOpen‘(ℝ^‘𝑋)) |
65 | 64 | rrxtop 40509 |
. . . . . . 7
⊢ (𝑋 ∈ Fin →
(TopOpen‘(ℝ^‘𝑋)) ∈ Top) |
66 | 25, 65 | syl 17 |
. . . . . 6
⊢ (𝜑 →
(TopOpen‘(ℝ^‘𝑋)) ∈ Top) |
67 | 66 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) →
(TopOpen‘(ℝ^‘𝑋)) ∈ Top) |
68 | | eltop2 20779 |
. . . . 5
⊢
((TopOpen‘(ℝ^‘𝑋)) ∈ Top → (X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∈
(TopOpen‘(ℝ^‘𝑋)) ↔ ∀𝑓 ∈ X 𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝑓 ∈ 𝑣 ∧ 𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))))) |
69 | 67, 68 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∈
(TopOpen‘(ℝ^‘𝑋)) ↔ ∀𝑓 ∈ X 𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝑓 ∈ 𝑣 ∧ 𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))))) |
70 | 63, 69 | mpbird 247 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∈
(TopOpen‘(ℝ^‘𝑋))) |
71 | 17, 70 | syldan 487 |
. 2
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∈
(TopOpen‘(ℝ^‘𝑋))) |
72 | 15, 71 | pm2.61dan 832 |
1
⊢ (𝜑 → X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∈
(TopOpen‘(ℝ^‘𝑋))) |