Proof of Theorem ioorrnopnlem
Step | Hyp | Ref
| Expression |
1 | | ioorrnopnlem.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ Fin) |
2 | | ioorrnopnlem.d |
. . . . 5
⊢ 𝐷 = (𝑓 ∈ (ℝ ↑𝑚
𝑋), 𝑔 ∈ (ℝ ↑𝑚
𝑋) ↦
(√‘Σ𝑘
∈ 𝑋 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))) |
3 | 1, 2 | rrndsxmet 41439 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ (∞Met‘(ℝ
↑𝑚 𝑋))) |
4 | | nfv 1957 |
. . . . . 6
⊢
Ⅎ𝑖𝜑 |
5 | | reex 10363 |
. . . . . . 7
⊢ ℝ
∈ V |
6 | 5 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℝ ∈
V) |
7 | | ioossre 12547 |
. . . . . . 7
⊢ ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ⊆ ℝ |
8 | 7 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ⊆ ℝ) |
9 | 4, 6, 8 | ixpssmapc 40166 |
. . . . 5
⊢ (𝜑 → X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ⊆ (ℝ
↑𝑚 𝑋)) |
10 | | ioorrnopnlem.f |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
11 | 9, 10 | sseldd 3821 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (ℝ ↑𝑚
𝑋)) |
12 | | ioorrnopnlem.e |
. . . . . 6
⊢ 𝐸 = inf(𝐻, ℝ, < ) |
13 | | ioorrnopnlem.h |
. . . . . . . . 9
⊢ 𝐻 = ran (𝑖 ∈ 𝑋 ↦ if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖)))) |
14 | 13 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 = ran (𝑖 ∈ 𝑋 ↦ if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))))) |
15 | | ioorrnopnlem.b |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵:𝑋⟶ℝ) |
16 | 15 | ffvelrnda 6623 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈ ℝ) |
17 | 10 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝐹 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
18 | | simpr 479 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋) |
19 | | fvixp2 40303 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) ∈ ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
20 | 17, 18, 19 | syl2anc 579 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) ∈ ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
21 | 7, 20 | sseldi 3818 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) ∈ ℝ) |
22 | 16, 21 | resubcld 10803 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐵‘𝑖) − (𝐹‘𝑖)) ∈ ℝ) |
23 | | ioorrnopnlem.a |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴:𝑋⟶ℝ) |
24 | 23 | ffvelrnda 6623 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈ ℝ) |
25 | 24 | rexrd 10426 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈
ℝ*) |
26 | 16 | rexrd 10426 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈
ℝ*) |
27 | | iooltub 40637 |
. . . . . . . . . . . . . 14
⊢ (((𝐴‘𝑖) ∈ ℝ* ∧ (𝐵‘𝑖) ∈ ℝ* ∧ (𝐹‘𝑖) ∈ ((𝐴‘𝑖)(,)(𝐵‘𝑖))) → (𝐹‘𝑖) < (𝐵‘𝑖)) |
28 | 25, 26, 20, 27 | syl3anc 1439 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) < (𝐵‘𝑖)) |
29 | 21, 16 | posdifd 10962 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) < (𝐵‘𝑖) ↔ 0 < ((𝐵‘𝑖) − (𝐹‘𝑖)))) |
30 | 28, 29 | mpbid 224 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 0 < ((𝐵‘𝑖) − (𝐹‘𝑖))) |
31 | 22, 30 | elrpd 12178 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐵‘𝑖) − (𝐹‘𝑖)) ∈
ℝ+) |
32 | 21, 24 | resubcld 10803 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) − (𝐴‘𝑖)) ∈ ℝ) |
33 | | ioogtlb 40621 |
. . . . . . . . . . . . . 14
⊢ (((𝐴‘𝑖) ∈ ℝ* ∧ (𝐵‘𝑖) ∈ ℝ* ∧ (𝐹‘𝑖) ∈ ((𝐴‘𝑖)(,)(𝐵‘𝑖))) → (𝐴‘𝑖) < (𝐹‘𝑖)) |
34 | 25, 26, 20, 33 | syl3anc 1439 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) < (𝐹‘𝑖)) |
35 | 24, 21 | posdifd 10962 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐴‘𝑖) < (𝐹‘𝑖) ↔ 0 < ((𝐹‘𝑖) − (𝐴‘𝑖)))) |
36 | 34, 35 | mpbid 224 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 0 < ((𝐹‘𝑖) − (𝐴‘𝑖))) |
37 | 32, 36 | elrpd 12178 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) − (𝐴‘𝑖)) ∈
ℝ+) |
38 | 31, 37 | ifcld 4351 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))) ∈
ℝ+) |
39 | 38 | ralrimiva 3147 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑖 ∈ 𝑋 if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))) ∈
ℝ+) |
40 | | eqid 2777 |
. . . . . . . . . 10
⊢ (𝑖 ∈ 𝑋 ↦ if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖)))) = (𝑖 ∈ 𝑋 ↦ if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖)))) |
41 | 40 | rnmptss 6656 |
. . . . . . . . 9
⊢
(∀𝑖 ∈
𝑋 if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))) ∈ ℝ+ → ran
(𝑖 ∈ 𝑋 ↦ if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖)))) ⊆
ℝ+) |
42 | 39, 41 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ran (𝑖 ∈ 𝑋 ↦ if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖)))) ⊆
ℝ+) |
43 | 14, 42 | eqsstrd 3857 |
. . . . . . 7
⊢ (𝜑 → 𝐻 ⊆
ℝ+) |
44 | | ltso 10457 |
. . . . . . . . 9
⊢ < Or
ℝ |
45 | 44 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → < Or
ℝ) |
46 | 40 | rnmptfi 40267 |
. . . . . . . . . 10
⊢ (𝑋 ∈ Fin → ran (𝑖 ∈ 𝑋 ↦ if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖)))) ∈ Fin) |
47 | 1, 46 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ran (𝑖 ∈ 𝑋 ↦ if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖)))) ∈ Fin) |
48 | 13, 47 | syl5eqel 2862 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 ∈ Fin) |
49 | 38 | elexd 3415 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))) ∈ V) |
50 | | ioorrnopnlem.n |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ≠ ∅) |
51 | 4, 49, 40, 50 | rnmptn0 40326 |
. . . . . . . . 9
⊢ (𝜑 → ran (𝑖 ∈ 𝑋 ↦ if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖)))) ≠ ∅) |
52 | 14, 51 | eqnetrd 3035 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 ≠ ∅) |
53 | | rpssre 12144 |
. . . . . . . . . 10
⊢
ℝ+ ⊆ ℝ |
54 | 53 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ℝ+
⊆ ℝ) |
55 | 43, 54 | sstrd 3830 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 ⊆ ℝ) |
56 | | fiinfcl 8695 |
. . . . . . . 8
⊢ (( <
Or ℝ ∧ (𝐻 ∈
Fin ∧ 𝐻 ≠ ∅
∧ 𝐻 ⊆ ℝ))
→ inf(𝐻, ℝ, <
) ∈ 𝐻) |
57 | 45, 48, 52, 55, 56 | syl13anc 1440 |
. . . . . . 7
⊢ (𝜑 → inf(𝐻, ℝ, < ) ∈ 𝐻) |
58 | 43, 57 | sseldd 3821 |
. . . . . 6
⊢ (𝜑 → inf(𝐻, ℝ, < ) ∈
ℝ+) |
59 | 12, 58 | syl5eqel 2862 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
60 | | rpxr 12148 |
. . . . 5
⊢ (𝐸 ∈ ℝ+
→ 𝐸 ∈
ℝ*) |
61 | 59, 60 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐸 ∈
ℝ*) |
62 | | eqid 2777 |
. . . . 5
⊢
(MetOpen‘𝐷) =
(MetOpen‘𝐷) |
63 | 62 | blopn 22713 |
. . . 4
⊢ ((𝐷 ∈
(∞Met‘(ℝ ↑𝑚 𝑋)) ∧ 𝐹 ∈ (ℝ ↑𝑚
𝑋) ∧ 𝐸 ∈ ℝ*) → (𝐹(ball‘𝐷)𝐸) ∈ (MetOpen‘𝐷)) |
64 | 3, 11, 61, 63 | syl3anc 1439 |
. . 3
⊢ (𝜑 → (𝐹(ball‘𝐷)𝐸) ∈ (MetOpen‘𝐷)) |
65 | | ioorrnopnlem.v |
. . . . 5
⊢ 𝑉 = (𝐹(ball‘𝐷)𝐸) |
66 | 65 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑉 = (𝐹(ball‘𝐷)𝐸)) |
67 | 1 | rrxtopnfi 41423 |
. . . . 5
⊢ (𝜑 →
(TopOpen‘(ℝ^‘𝑋)) = (MetOpen‘(𝑓 ∈ (ℝ ↑𝑚
𝑋), 𝑔 ∈ (ℝ ↑𝑚
𝑋) ↦
(√‘Σ𝑘
∈ 𝑋 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))))) |
68 | 2 | eqcomi 2786 |
. . . . . . 7
⊢ (𝑓 ∈ (ℝ
↑𝑚 𝑋), 𝑔 ∈ (ℝ ↑𝑚
𝑋) ↦
(√‘Σ𝑘
∈ 𝑋 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))) = 𝐷 |
69 | 68 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝑓 ∈ (ℝ ↑𝑚
𝑋), 𝑔 ∈ (ℝ ↑𝑚
𝑋) ↦
(√‘Σ𝑘
∈ 𝑋 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))) = 𝐷) |
70 | 69 | fveq2d 6450 |
. . . . 5
⊢ (𝜑 → (MetOpen‘(𝑓 ∈ (ℝ
↑𝑚 𝑋), 𝑔 ∈ (ℝ ↑𝑚
𝑋) ↦
(√‘Σ𝑘
∈ 𝑋 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)))) = (MetOpen‘𝐷)) |
71 | 67, 70 | eqtrd 2813 |
. . . 4
⊢ (𝜑 →
(TopOpen‘(ℝ^‘𝑋)) = (MetOpen‘𝐷)) |
72 | 66, 71 | eleq12d 2852 |
. . 3
⊢ (𝜑 → (𝑉 ∈ (TopOpen‘(ℝ^‘𝑋)) ↔ (𝐹(ball‘𝐷)𝐸) ∈ (MetOpen‘𝐷))) |
73 | 64, 72 | mpbird 249 |
. 2
⊢ (𝜑 → 𝑉 ∈ (TopOpen‘(ℝ^‘𝑋))) |
74 | | xmetpsmet 22561 |
. . . . . 6
⊢ (𝐷 ∈
(∞Met‘(ℝ ↑𝑚 𝑋)) → 𝐷 ∈ (PsMet‘(ℝ
↑𝑚 𝑋))) |
75 | 3, 74 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ (PsMet‘(ℝ
↑𝑚 𝑋))) |
76 | | blcntrps 22625 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘(ℝ
↑𝑚 𝑋)) ∧ 𝐹 ∈ (ℝ ↑𝑚
𝑋) ∧ 𝐸 ∈ ℝ+) → 𝐹 ∈ (𝐹(ball‘𝐷)𝐸)) |
77 | 75, 11, 59, 76 | syl3anc 1439 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (𝐹(ball‘𝐷)𝐸)) |
78 | 66 | eqcomd 2783 |
. . . 4
⊢ (𝜑 → (𝐹(ball‘𝐷)𝐸) = 𝑉) |
79 | 77, 78 | eleqtrd 2860 |
. . 3
⊢ (𝜑 → 𝐹 ∈ 𝑉) |
80 | | nfv 1957 |
. . . . 5
⊢
Ⅎ𝑔𝜑 |
81 | | elmapfn 8163 |
. . . . . . . 8
⊢ (𝑔 ∈ (ℝ
↑𝑚 𝑋) → 𝑔 Fn 𝑋) |
82 | 81 | 3ad2ant2 1125 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) → 𝑔 Fn 𝑋) |
83 | 25 | 3ad2antl1 1193 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈
ℝ*) |
84 | 26 | 3ad2antl1 1193 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈
ℝ*) |
85 | | simpl2 1201 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → 𝑔 ∈ (ℝ ↑𝑚
𝑋)) |
86 | | simpr 479 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋) |
87 | | elmapi 8162 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈ (ℝ
↑𝑚 𝑋) → 𝑔:𝑋⟶ℝ) |
88 | 87 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝑔 ∈ (ℝ
↑𝑚 𝑋) ∧ 𝑖 ∈ 𝑋) → 𝑔:𝑋⟶ℝ) |
89 | | simpr 479 |
. . . . . . . . . . 11
⊢ ((𝑔 ∈ (ℝ
↑𝑚 𝑋) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋) |
90 | 88, 89 | ffvelrnd 6624 |
. . . . . . . . . 10
⊢ ((𝑔 ∈ (ℝ
↑𝑚 𝑋) ∧ 𝑖 ∈ 𝑋) → (𝑔‘𝑖) ∈ ℝ) |
91 | 85, 86, 90 | syl2anc 579 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → (𝑔‘𝑖) ∈ ℝ) |
92 | 24 | 3ad2antl1 1193 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈ ℝ) |
93 | 53, 59 | sseldi 3818 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐸 ∈ ℝ) |
94 | 93 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝐸 ∈ ℝ) |
95 | 21, 94 | resubcld 10803 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) − 𝐸) ∈ ℝ) |
96 | 95 | 3ad2antl1 1193 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) − 𝐸) ∈ ℝ) |
97 | 53, 38 | sseldi 3818 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))) ∈ ℝ) |
98 | 12 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐸 = inf(𝐻, ℝ, < )) |
99 | | infxrrefi 40501 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐻 ⊆ ℝ ∧ 𝐻 ∈ Fin ∧ 𝐻 ≠ ∅) → inf(𝐻, ℝ*, < ) =
inf(𝐻, ℝ, <
)) |
100 | 55, 48, 52, 99 | syl3anc 1439 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → inf(𝐻, ℝ*, < ) = inf(𝐻, ℝ, <
)) |
101 | 100 | eqcomd 2783 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → inf(𝐻, ℝ, < ) = inf(𝐻, ℝ*, <
)) |
102 | 98, 101 | eqtrd 2813 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐸 = inf(𝐻, ℝ*, <
)) |
103 | 102 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝐸 = inf(𝐻, ℝ*, <
)) |
104 | | ressxr 10420 |
. . . . . . . . . . . . . . . . . 18
⊢ ℝ
⊆ ℝ* |
105 | 104 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ℝ ⊆
ℝ*) |
106 | 55, 105 | sstrd 3830 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐻 ⊆
ℝ*) |
107 | 106 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝐻 ⊆
ℝ*) |
108 | 40 | elrnmpt1 5620 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ 𝑋 ∧ if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))) ∈ V) → if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))) ∈ ran (𝑖 ∈ 𝑋 ↦ if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))))) |
109 | 18, 49, 108 | syl2anc 579 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))) ∈ ran (𝑖 ∈ 𝑋 ↦ if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))))) |
110 | 109, 13 | syl6eleqr 2869 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))) ∈ 𝐻) |
111 | | infxrlb 12476 |
. . . . . . . . . . . . . . 15
⊢ ((𝐻 ⊆ ℝ*
∧ if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))) ∈ 𝐻) → inf(𝐻, ℝ*, < ) ≤
if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖)))) |
112 | 107, 110,
111 | syl2anc 579 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → inf(𝐻, ℝ*, < ) ≤
if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖)))) |
113 | 103, 112 | eqbrtrd 4908 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝐸 ≤ if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖)))) |
114 | | min2 12333 |
. . . . . . . . . . . . . 14
⊢ ((((𝐵‘𝑖) − (𝐹‘𝑖)) ∈ ℝ ∧ ((𝐹‘𝑖) − (𝐴‘𝑖)) ∈ ℝ) → if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖))) |
115 | 22, 32, 114 | syl2anc 579 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖))) |
116 | 94, 97, 32, 113, 115 | letrd 10533 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝐸 ≤ ((𝐹‘𝑖) − (𝐴‘𝑖))) |
117 | 94, 21, 24, 116 | lesubd 10979 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ≤ ((𝐹‘𝑖) − 𝐸)) |
118 | 117 | 3ad2antl1 1193 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ≤ ((𝐹‘𝑖) − 𝐸)) |
119 | 21 | adantlr 705 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) ∈ ℝ) |
120 | 90 | adantll 704 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → (𝑔‘𝑖) ∈ ℝ) |
121 | 119, 120 | resubcld 10803 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) − (𝑔‘𝑖)) ∈ ℝ) |
122 | 121 | 3adantl3 1170 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) − (𝑔‘𝑖)) ∈ ℝ) |
123 | 1, 2 | rrndsmet 41438 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐷 ∈ (Met‘(ℝ
↑𝑚 𝑋))) |
124 | 123 | ad2antrr 716 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → 𝐷 ∈ (Met‘(ℝ
↑𝑚 𝑋))) |
125 | 11 | ad2antrr 716 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → 𝐹 ∈ (ℝ ↑𝑚
𝑋)) |
126 | | simplr 759 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → 𝑔 ∈ (ℝ ↑𝑚
𝑋)) |
127 | | metcl 22545 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (Met‘(ℝ
↑𝑚 𝑋)) ∧ 𝐹 ∈ (ℝ ↑𝑚
𝑋) ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) → (𝐹𝐷𝑔) ∈ ℝ) |
128 | 124, 125,
126, 127 | syl3anc 1439 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → (𝐹𝐷𝑔) ∈ ℝ) |
129 | 128 | 3adantl3 1170 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → (𝐹𝐷𝑔) ∈ ℝ) |
130 | 94 | adantlr 705 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → 𝐸 ∈ ℝ) |
131 | 130 | 3adantl3 1170 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → 𝐸 ∈ ℝ) |
132 | 121 | recnd 10405 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) − (𝑔‘𝑖)) ∈ ℂ) |
133 | 132 | abscld 14583 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → (abs‘((𝐹‘𝑖) − (𝑔‘𝑖))) ∈ ℝ) |
134 | 121 | leabsd 14561 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) − (𝑔‘𝑖)) ≤ (abs‘((𝐹‘𝑖) − (𝑔‘𝑖)))) |
135 | 1 | ad2antrr 716 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → 𝑋 ∈ Fin) |
136 | | ixpf 8216 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 ∈ X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) → 𝐹:𝑋⟶∪
𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
137 | 10, 136 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹:𝑋⟶∪
𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
138 | 8 | ralrimiva 3147 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∀𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ⊆ ℝ) |
139 | | iunss 4794 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∪ 𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ⊆ ℝ ↔ ∀𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ⊆ ℝ) |
140 | 138, 139 | sylibr 226 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∪ 𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ⊆ ℝ) |
141 | 137, 140 | fssd 6305 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹:𝑋⟶ℝ) |
142 | 141 | ad2antrr 716 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → 𝐹:𝑋⟶ℝ) |
143 | 126, 87 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → 𝑔:𝑋⟶ℝ) |
144 | | simpr 479 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋) |
145 | | eqid 2777 |
. . . . . . . . . . . . . . . 16
⊢
(dist‘(ℝ^‘𝑋)) = (dist‘(ℝ^‘𝑋)) |
146 | 135, 142,
143, 144, 145 | rrnprjdstle 41437 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → (abs‘((𝐹‘𝑖) − (𝑔‘𝑖))) ≤ (𝐹(dist‘(ℝ^‘𝑋))𝑔)) |
147 | | eqid 2777 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(ℝ^‘𝑋) =
(ℝ^‘𝑋) |
148 | | eqid 2777 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (ℝ
↑𝑚 𝑋) = (ℝ ↑𝑚
𝑋) |
149 | 147, 148 | rrxdsfi 23617 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑋 ∈ Fin →
(dist‘(ℝ^‘𝑋)) = (𝑓 ∈ (ℝ ↑𝑚
𝑋), 𝑔 ∈ (ℝ ↑𝑚
𝑋) ↦
(√‘Σ𝑘
∈ 𝑋 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)))) |
150 | 1, 149 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
(dist‘(ℝ^‘𝑋)) = (𝑓 ∈ (ℝ ↑𝑚
𝑋), 𝑔 ∈ (ℝ ↑𝑚
𝑋) ↦
(√‘Σ𝑘
∈ 𝑋 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)))) |
151 | 150, 69 | eqtrd 2813 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
(dist‘(ℝ^‘𝑋)) = 𝐷) |
152 | 151 | oveqd 6939 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐹(dist‘(ℝ^‘𝑋))𝑔) = (𝐹𝐷𝑔)) |
153 | 152 | ad2antrr 716 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → (𝐹(dist‘(ℝ^‘𝑋))𝑔) = (𝐹𝐷𝑔)) |
154 | 146, 153 | breqtrd 4912 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → (abs‘((𝐹‘𝑖) − (𝑔‘𝑖))) ≤ (𝐹𝐷𝑔)) |
155 | 121, 133,
128, 134, 154 | letrd 10533 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) − (𝑔‘𝑖)) ≤ (𝐹𝐷𝑔)) |
156 | 155 | 3adantl3 1170 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) − (𝑔‘𝑖)) ≤ (𝐹𝐷𝑔)) |
157 | | simpl3 1203 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → (𝐹𝐷𝑔) < 𝐸) |
158 | 122, 129,
131, 156, 157 | lelttrd 10534 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) − (𝑔‘𝑖)) < 𝐸) |
159 | | ltsub23 10855 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑖) ∈ ℝ ∧ (𝑔‘𝑖) ∈ ℝ ∧ 𝐸 ∈ ℝ) → (((𝐹‘𝑖) − (𝑔‘𝑖)) < 𝐸 ↔ ((𝐹‘𝑖) − 𝐸) < (𝑔‘𝑖))) |
160 | 119, 120,
130, 159 | syl3anc 1439 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → (((𝐹‘𝑖) − (𝑔‘𝑖)) < 𝐸 ↔ ((𝐹‘𝑖) − 𝐸) < (𝑔‘𝑖))) |
161 | 160 | 3adantl3 1170 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → (((𝐹‘𝑖) − (𝑔‘𝑖)) < 𝐸 ↔ ((𝐹‘𝑖) − 𝐸) < (𝑔‘𝑖))) |
162 | 158, 161 | mpbid 224 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) − 𝐸) < (𝑔‘𝑖)) |
163 | 92, 96, 91, 118, 162 | lelttrd 10534 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) < (𝑔‘𝑖)) |
164 | 21, 94 | readdcld 10406 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) + 𝐸) ∈ ℝ) |
165 | 164 | 3ad2antl1 1193 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) + 𝐸) ∈ ℝ) |
166 | 16 | 3ad2antl1 1193 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈ ℝ) |
167 | 120, 119 | resubcld 10803 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → ((𝑔‘𝑖) − (𝐹‘𝑖)) ∈ ℝ) |
168 | 167 | 3adantl3 1170 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → ((𝑔‘𝑖) − (𝐹‘𝑖)) ∈ ℝ) |
169 | 167 | leabsd 14561 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → ((𝑔‘𝑖) − (𝐹‘𝑖)) ≤ (abs‘((𝑔‘𝑖) − (𝐹‘𝑖)))) |
170 | 120 | recnd 10405 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → (𝑔‘𝑖) ∈ ℂ) |
171 | 119 | recnd 10405 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) ∈ ℂ) |
172 | 170, 171 | abssubd 14600 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → (abs‘((𝑔‘𝑖) − (𝐹‘𝑖))) = (abs‘((𝐹‘𝑖) − (𝑔‘𝑖)))) |
173 | 169, 172 | breqtrd 4912 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → ((𝑔‘𝑖) − (𝐹‘𝑖)) ≤ (abs‘((𝐹‘𝑖) − (𝑔‘𝑖)))) |
174 | 167, 133,
128, 173, 154 | letrd 10533 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → ((𝑔‘𝑖) − (𝐹‘𝑖)) ≤ (𝐹𝐷𝑔)) |
175 | 174 | 3adantl3 1170 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → ((𝑔‘𝑖) − (𝐹‘𝑖)) ≤ (𝐹𝐷𝑔)) |
176 | 168, 129,
131, 175, 157 | lelttrd 10534 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → ((𝑔‘𝑖) − (𝐹‘𝑖)) < 𝐸) |
177 | 119 | 3adantl3 1170 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) ∈ ℝ) |
178 | 91, 177, 131 | ltsubadd2d 10973 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → (((𝑔‘𝑖) − (𝐹‘𝑖)) < 𝐸 ↔ (𝑔‘𝑖) < ((𝐹‘𝑖) + 𝐸))) |
179 | 176, 178 | mpbid 224 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → (𝑔‘𝑖) < ((𝐹‘𝑖) + 𝐸)) |
180 | | min1 12332 |
. . . . . . . . . . . . . 14
⊢ ((((𝐵‘𝑖) − (𝐹‘𝑖)) ∈ ℝ ∧ ((𝐹‘𝑖) − (𝐴‘𝑖)) ∈ ℝ) → if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))) ≤ ((𝐵‘𝑖) − (𝐹‘𝑖))) |
181 | 22, 32, 180 | syl2anc 579 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))) ≤ ((𝐵‘𝑖) − (𝐹‘𝑖))) |
182 | 94, 97, 22, 113, 181 | letrd 10533 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝐸 ≤ ((𝐵‘𝑖) − (𝐹‘𝑖))) |
183 | 21, 94, 16 | leaddsub2d 10977 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (((𝐹‘𝑖) + 𝐸) ≤ (𝐵‘𝑖) ↔ 𝐸 ≤ ((𝐵‘𝑖) − (𝐹‘𝑖)))) |
184 | 182, 183 | mpbird 249 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) + 𝐸) ≤ (𝐵‘𝑖)) |
185 | 184 | 3ad2antl1 1193 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) + 𝐸) ≤ (𝐵‘𝑖)) |
186 | 91, 165, 166, 179, 185 | ltletrd 10536 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → (𝑔‘𝑖) < (𝐵‘𝑖)) |
187 | 83, 84, 91, 163, 186 | eliood 40624 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → (𝑔‘𝑖) ∈ ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
188 | 187 | ralrimiva 3147 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) → ∀𝑖 ∈ 𝑋 (𝑔‘𝑖) ∈ ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
189 | 82, 188 | jca 507 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) → (𝑔 Fn 𝑋 ∧ ∀𝑖 ∈ 𝑋 (𝑔‘𝑖) ∈ ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) |
190 | | vex 3400 |
. . . . . . 7
⊢ 𝑔 ∈ V |
191 | 190 | elixp 8201 |
. . . . . 6
⊢ (𝑔 ∈ X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ↔ (𝑔 Fn 𝑋 ∧ ∀𝑖 ∈ 𝑋 (𝑔‘𝑖) ∈ ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) |
192 | 189, 191 | sylibr 226 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) → 𝑔 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
193 | 80, 75, 11, 61, 192 | ballss3 40193 |
. . . 4
⊢ (𝜑 → (𝐹(ball‘𝐷)𝐸) ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
194 | 66, 193 | eqsstrd 3857 |
. . 3
⊢ (𝜑 → 𝑉 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
195 | 79, 194 | jca 507 |
. 2
⊢ (𝜑 → (𝐹 ∈ 𝑉 ∧ 𝑉 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) |
196 | | eleq2 2847 |
. . . 4
⊢ (𝑣 = 𝑉 → (𝐹 ∈ 𝑣 ↔ 𝐹 ∈ 𝑉)) |
197 | | sseq1 3844 |
. . . 4
⊢ (𝑣 = 𝑉 → (𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ↔ 𝑉 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) |
198 | 196, 197 | anbi12d 624 |
. . 3
⊢ (𝑣 = 𝑉 → ((𝐹 ∈ 𝑣 ∧ 𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) ↔ (𝐹 ∈ 𝑉 ∧ 𝑉 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))))) |
199 | 198 | rspcev 3510 |
. 2
⊢ ((𝑉 ∈
(TopOpen‘(ℝ^‘𝑋)) ∧ (𝐹 ∈ 𝑉 ∧ 𝑉 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) → ∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝐹 ∈ 𝑣 ∧ 𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) |
200 | 73, 195, 199 | syl2anc 579 |
1
⊢ (𝜑 → ∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝐹 ∈ 𝑣 ∧ 𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) |