Proof of Theorem ioorrnopnlem
Step | Hyp | Ref
| Expression |
1 | | ioorrnopnlem.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ Fin) |
2 | | ioorrnopnlem.d |
. . . . 5
⊢ 𝐷 = (𝑓 ∈ (ℝ ↑𝑚
𝑋), 𝑔 ∈ (ℝ ↑𝑚
𝑋) ↦
(√‘Σ𝑘
∈ 𝑋 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))) |
3 | 1, 2 | rrndsxmet 40523 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ (∞Met‘(ℝ
↑𝑚 𝑋))) |
4 | | nfv 1843 |
. . . . . 6
⊢
Ⅎ𝑖𝜑 |
5 | | reex 10027 |
. . . . . . 7
⊢ ℝ
∈ V |
6 | 5 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℝ ∈
V) |
7 | | ioossre 12235 |
. . . . . . 7
⊢ ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ⊆ ℝ |
8 | 7 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ⊆ ℝ) |
9 | 4, 6, 8 | ixpssmapc 39243 |
. . . . 5
⊢ (𝜑 → X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ⊆ (ℝ
↑𝑚 𝑋)) |
10 | | ioorrnopnlem.f |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
11 | 9, 10 | sseldd 3604 |
. . . 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 6359 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈ ℝ) |
17 | 10 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝐹 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
18 | | simpr 477 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋) |
19 | | fvixp2 39389 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) ∈ ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
20 | 17, 18, 19 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) ∈ ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
21 | 7, 20 | sseldi 3601 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) ∈ ℝ) |
22 | 16, 21 | resubcld 10458 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐵‘𝑖) − (𝐹‘𝑖)) ∈ ℝ) |
23 | | ioorrnopnlem.a |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴:𝑋⟶ℝ) |
24 | 23 | ffvelrnda 6359 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈ ℝ) |
25 | 24 | rexrd 10089 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈
ℝ*) |
26 | 16 | rexrd 10089 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈
ℝ*) |
27 | | iooltub 39735 |
. . . . . . . . . . . . . 14
⊢ (((𝐴‘𝑖) ∈ ℝ* ∧ (𝐵‘𝑖) ∈ ℝ* ∧ (𝐹‘𝑖) ∈ ((𝐴‘𝑖)(,)(𝐵‘𝑖))) → (𝐹‘𝑖) < (𝐵‘𝑖)) |
28 | 25, 26, 20, 27 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) < (𝐵‘𝑖)) |
29 | 21, 16 | posdifd 10614 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) < (𝐵‘𝑖) ↔ 0 < ((𝐵‘𝑖) − (𝐹‘𝑖)))) |
30 | 28, 29 | mpbid 222 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 0 < ((𝐵‘𝑖) − (𝐹‘𝑖))) |
31 | 22, 30 | elrpd 11869 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐵‘𝑖) − (𝐹‘𝑖)) ∈
ℝ+) |
32 | 21, 24 | resubcld 10458 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) − (𝐴‘𝑖)) ∈ ℝ) |
33 | | ioogtlb 39717 |
. . . . . . . . . . . . . 14
⊢ (((𝐴‘𝑖) ∈ ℝ* ∧ (𝐵‘𝑖) ∈ ℝ* ∧ (𝐹‘𝑖) ∈ ((𝐴‘𝑖)(,)(𝐵‘𝑖))) → (𝐴‘𝑖) < (𝐹‘𝑖)) |
34 | 25, 26, 20, 33 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) < (𝐹‘𝑖)) |
35 | 24, 21 | posdifd 10614 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐴‘𝑖) < (𝐹‘𝑖) ↔ 0 < ((𝐹‘𝑖) − (𝐴‘𝑖)))) |
36 | 34, 35 | mpbid 222 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 0 < ((𝐹‘𝑖) − (𝐴‘𝑖))) |
37 | 32, 36 | elrpd 11869 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) − (𝐴‘𝑖)) ∈
ℝ+) |
38 | 31, 37 | ifcld 4131 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))) ∈
ℝ+) |
39 | 38 | ralrimiva 2966 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑖 ∈ 𝑋 if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))) ∈
ℝ+) |
40 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑖 ∈ 𝑋 ↦ if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖)))) = (𝑖 ∈ 𝑋 ↦ if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖)))) |
41 | 40 | rnmptss 6392 |
. . . . . . . . 9
⊢
(∀𝑖 ∈
𝑋 if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))) ∈ ℝ+ → ran
(𝑖 ∈ 𝑋 ↦ if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖)))) ⊆
ℝ+) |
42 | 39, 41 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ran (𝑖 ∈ 𝑋 ↦ if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖)))) ⊆
ℝ+) |
43 | 14, 42 | eqsstrd 3639 |
. . . . . . 7
⊢ (𝜑 → 𝐻 ⊆
ℝ+) |
44 | | ltso 10118 |
. . . . . . . . 9
⊢ < Or
ℝ |
45 | 44 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → < Or
ℝ) |
46 | 40 | rnmptfi 39351 |
. . . . . . . . . 10
⊢ (𝑋 ∈ Fin → ran (𝑖 ∈ 𝑋 ↦ if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖)))) ∈ Fin) |
47 | 1, 46 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ran (𝑖 ∈ 𝑋 ↦ if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖)))) ∈ Fin) |
48 | 13, 47 | syl5eqel 2705 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 ∈ Fin) |
49 | 38 | elexd 3214 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))) ∈ V) |
50 | | ioorrnopnlem.n |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ≠ ∅) |
51 | 4, 49, 40, 50 | rnmptn0 39413 |
. . . . . . . . 9
⊢ (𝜑 → ran (𝑖 ∈ 𝑋 ↦ if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖)))) ≠ ∅) |
52 | 14, 51 | eqnetrd 2861 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 ≠ ∅) |
53 | | rpssre 11843 |
. . . . . . . . . 10
⊢
ℝ+ ⊆ ℝ |
54 | 53 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ℝ+
⊆ ℝ) |
55 | 43, 54 | sstrd 3613 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 ⊆ ℝ) |
56 | | fiinfcl 8407 |
. . . . . . . 8
⊢ (( <
Or ℝ ∧ (𝐻 ∈
Fin ∧ 𝐻 ≠ ∅
∧ 𝐻 ⊆ ℝ))
→ inf(𝐻, ℝ, <
) ∈ 𝐻) |
57 | 45, 48, 52, 55, 56 | syl13anc 1328 |
. . . . . . 7
⊢ (𝜑 → inf(𝐻, ℝ, < ) ∈ 𝐻) |
58 | 43, 57 | sseldd 3604 |
. . . . . 6
⊢ (𝜑 → inf(𝐻, ℝ, < ) ∈
ℝ+) |
59 | 12, 58 | syl5eqel 2705 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
60 | | rpxr 11840 |
. . . . 5
⊢ (𝐸 ∈ ℝ+
→ 𝐸 ∈
ℝ*) |
61 | 59, 60 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐸 ∈
ℝ*) |
62 | | eqid 2622 |
. . . . 5
⊢
(MetOpen‘𝐷) =
(MetOpen‘𝐷) |
63 | 62 | blopn 22305 |
. . . 4
⊢ ((𝐷 ∈
(∞Met‘(ℝ ↑𝑚 𝑋)) ∧ 𝐹 ∈ (ℝ ↑𝑚
𝑋) ∧ 𝐸 ∈ ℝ*) → (𝐹(ball‘𝐷)𝐸) ∈ (MetOpen‘𝐷)) |
64 | 3, 11, 61, 63 | syl3anc 1326 |
. . 3
⊢ (𝜑 → (𝐹(ball‘𝐷)𝐸) ∈ (MetOpen‘𝐷)) |
65 | | ioorrnopnlem.v |
. . . . 5
⊢ 𝑉 = (𝐹(ball‘𝐷)𝐸) |
66 | 65 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑉 = (𝐹(ball‘𝐷)𝐸)) |
67 | 1 | rrxtopnfi 40506 |
. . . . 5
⊢ (𝜑 →
(TopOpen‘(ℝ^‘𝑋)) = (MetOpen‘(𝑓 ∈ (ℝ ↑𝑚
𝑋), 𝑔 ∈ (ℝ ↑𝑚
𝑋) ↦
(√‘Σ𝑘
∈ 𝑋 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))))) |
68 | 2 | eqcomi 2631 |
. . . . . . 7
⊢ (𝑓 ∈ (ℝ
↑𝑚 𝑋), 𝑔 ∈ (ℝ ↑𝑚
𝑋) ↦
(√‘Σ𝑘
∈ 𝑋 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))) = 𝐷 |
69 | 68 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝑓 ∈ (ℝ ↑𝑚
𝑋), 𝑔 ∈ (ℝ ↑𝑚
𝑋) ↦
(√‘Σ𝑘
∈ 𝑋 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))) = 𝐷) |
70 | 69 | fveq2d 6195 |
. . . . 5
⊢ (𝜑 → (MetOpen‘(𝑓 ∈ (ℝ
↑𝑚 𝑋), 𝑔 ∈ (ℝ ↑𝑚
𝑋) ↦
(√‘Σ𝑘
∈ 𝑋 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)))) = (MetOpen‘𝐷)) |
71 | 67, 70 | eqtrd 2656 |
. . . 4
⊢ (𝜑 →
(TopOpen‘(ℝ^‘𝑋)) = (MetOpen‘𝐷)) |
72 | 66, 71 | eleq12d 2695 |
. . 3
⊢ (𝜑 → (𝑉 ∈ (TopOpen‘(ℝ^‘𝑋)) ↔ (𝐹(ball‘𝐷)𝐸) ∈ (MetOpen‘𝐷))) |
73 | 64, 72 | mpbird 247 |
. 2
⊢ (𝜑 → 𝑉 ∈ (TopOpen‘(ℝ^‘𝑋))) |
74 | | xmetpsmet 22153 |
. . . . . 6
⊢ (𝐷 ∈
(∞Met‘(ℝ ↑𝑚 𝑋)) → 𝐷 ∈ (PsMet‘(ℝ
↑𝑚 𝑋))) |
75 | 3, 74 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ (PsMet‘(ℝ
↑𝑚 𝑋))) |
76 | | blcntrps 22217 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘(ℝ
↑𝑚 𝑋)) ∧ 𝐹 ∈ (ℝ ↑𝑚
𝑋) ∧ 𝐸 ∈ ℝ+) → 𝐹 ∈ (𝐹(ball‘𝐷)𝐸)) |
77 | 75, 11, 59, 76 | syl3anc 1326 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (𝐹(ball‘𝐷)𝐸)) |
78 | 66 | eqcomd 2628 |
. . . 4
⊢ (𝜑 → (𝐹(ball‘𝐷)𝐸) = 𝑉) |
79 | 77, 78 | eleqtrd 2703 |
. . 3
⊢ (𝜑 → 𝐹 ∈ 𝑉) |
80 | | nfv 1843 |
. . . . 5
⊢
Ⅎ𝑔𝜑 |
81 | | elmapfn 7880 |
. . . . . . . 8
⊢ (𝑔 ∈ (ℝ
↑𝑚 𝑋) → 𝑔 Fn 𝑋) |
82 | 81 | 3ad2ant2 1083 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) → 𝑔 Fn 𝑋) |
83 | 25 | 3ad2antl1 1223 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈
ℝ*) |
84 | 26 | 3ad2antl1 1223 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈
ℝ*) |
85 | | simpl2 1065 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → 𝑔 ∈ (ℝ ↑𝑚
𝑋)) |
86 | | simpr 477 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋) |
87 | | elmapi 7879 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈ (ℝ
↑𝑚 𝑋) → 𝑔:𝑋⟶ℝ) |
88 | 87 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑔 ∈ (ℝ
↑𝑚 𝑋) ∧ 𝑖 ∈ 𝑋) → 𝑔:𝑋⟶ℝ) |
89 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((𝑔 ∈ (ℝ
↑𝑚 𝑋) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋) |
90 | 88, 89 | ffvelrnd 6360 |
. . . . . . . . . 10
⊢ ((𝑔 ∈ (ℝ
↑𝑚 𝑋) ∧ 𝑖 ∈ 𝑋) → (𝑔‘𝑖) ∈ ℝ) |
91 | 85, 86, 90 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → (𝑔‘𝑖) ∈ ℝ) |
92 | 24 | 3ad2antl1 1223 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈ ℝ) |
93 | 53, 59 | sseldi 3601 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐸 ∈ ℝ) |
94 | 93 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝐸 ∈ ℝ) |
95 | 21, 94 | resubcld 10458 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) − 𝐸) ∈ ℝ) |
96 | 95 | 3ad2antl1 1223 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) − 𝐸) ∈ ℝ) |
97 | 53, 38 | sseldi 3601 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))) ∈ ℝ) |
98 | 12 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐸 = inf(𝐻, ℝ, < )) |
99 | | infxrrefi 39601 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐻 ⊆ ℝ ∧ 𝐻 ∈ Fin ∧ 𝐻 ≠ ∅) → inf(𝐻, ℝ*, < ) =
inf(𝐻, ℝ, <
)) |
100 | 55, 48, 52, 99 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → inf(𝐻, ℝ*, < ) = inf(𝐻, ℝ, <
)) |
101 | 100 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → inf(𝐻, ℝ, < ) = inf(𝐻, ℝ*, <
)) |
102 | 98, 101 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐸 = inf(𝐻, ℝ*, <
)) |
103 | 102 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝐸 = inf(𝐻, ℝ*, <
)) |
104 | | ressxr 10083 |
. . . . . . . . . . . . . . . . . 18
⊢ ℝ
⊆ ℝ* |
105 | 104 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ℝ ⊆
ℝ*) |
106 | 55, 105 | sstrd 3613 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐻 ⊆
ℝ*) |
107 | 106 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝐻 ⊆
ℝ*) |
108 | 40 | elrnmpt1 5374 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ 𝑋 ∧ if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))) ∈ V) → if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))) ∈ ran (𝑖 ∈ 𝑋 ↦ if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))))) |
109 | 18, 49, 108 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))) ∈ ran (𝑖 ∈ 𝑋 ↦ if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))))) |
110 | 109, 13 | syl6eleqr 2712 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))) ∈ 𝐻) |
111 | | infxrlb 12164 |
. . . . . . . . . . . . . . 15
⊢ ((𝐻 ⊆ ℝ*
∧ if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))) ∈ 𝐻) → inf(𝐻, ℝ*, < ) ≤
if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖)))) |
112 | 107, 110,
111 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → inf(𝐻, ℝ*, < ) ≤
if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖)))) |
113 | 103, 112 | eqbrtrd 4675 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝐸 ≤ if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖)))) |
114 | | min2 12021 |
. . . . . . . . . . . . . 14
⊢ ((((𝐵‘𝑖) − (𝐹‘𝑖)) ∈ ℝ ∧ ((𝐹‘𝑖) − (𝐴‘𝑖)) ∈ ℝ) → if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖))) |
115 | 22, 32, 114 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖))) |
116 | 94, 97, 32, 113, 115 | letrd 10194 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝐸 ≤ ((𝐹‘𝑖) − (𝐴‘𝑖))) |
117 | 94, 21, 24, 116 | lesubd 10631 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ≤ ((𝐹‘𝑖) − 𝐸)) |
118 | 117 | 3ad2antl1 1223 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ≤ ((𝐹‘𝑖) − 𝐸)) |
119 | 21 | adantlr 751 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) ∈ ℝ) |
120 | 90 | adantll 750 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → (𝑔‘𝑖) ∈ ℝ) |
121 | 119, 120 | resubcld 10458 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) − (𝑔‘𝑖)) ∈ ℝ) |
122 | 121 | 3adantl3 1219 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) − (𝑔‘𝑖)) ∈ ℝ) |
123 | 1, 2 | rrndsmet 40522 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐷 ∈ (Met‘(ℝ
↑𝑚 𝑋))) |
124 | 123 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → 𝐷 ∈ (Met‘(ℝ
↑𝑚 𝑋))) |
125 | 11 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → 𝐹 ∈ (ℝ ↑𝑚
𝑋)) |
126 | | simplr 792 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → 𝑔 ∈ (ℝ ↑𝑚
𝑋)) |
127 | | metcl 22137 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (Met‘(ℝ
↑𝑚 𝑋)) ∧ 𝐹 ∈ (ℝ ↑𝑚
𝑋) ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) → (𝐹𝐷𝑔) ∈ ℝ) |
128 | 124, 125,
126, 127 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → (𝐹𝐷𝑔) ∈ ℝ) |
129 | 128 | 3adantl3 1219 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → (𝐹𝐷𝑔) ∈ ℝ) |
130 | 94 | adantlr 751 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → 𝐸 ∈ ℝ) |
131 | 130 | 3adantl3 1219 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → 𝐸 ∈ ℝ) |
132 | 121 | recnd 10068 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) − (𝑔‘𝑖)) ∈ ℂ) |
133 | 132 | abscld 14175 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → (abs‘((𝐹‘𝑖) − (𝑔‘𝑖))) ∈ ℝ) |
134 | 121 | leabsd 14153 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) − (𝑔‘𝑖)) ≤ (abs‘((𝐹‘𝑖) − (𝑔‘𝑖)))) |
135 | 1 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → 𝑋 ∈ Fin) |
136 | | ixpf 7930 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 ∈ X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) → 𝐹:𝑋⟶∪
𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
137 | 10, 136 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹:𝑋⟶∪
𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
138 | 8 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∀𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ⊆ ℝ) |
139 | | iunss 4561 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∪ 𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ⊆ ℝ ↔ ∀𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ⊆ ℝ) |
140 | 138, 139 | sylibr 224 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∪ 𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ⊆ ℝ) |
141 | 137, 140 | fssd 6057 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹:𝑋⟶ℝ) |
142 | 141 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → 𝐹:𝑋⟶ℝ) |
143 | 126, 87 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → 𝑔:𝑋⟶ℝ) |
144 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋) |
145 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
⊢
(dist‘(ℝ^‘𝑋)) = (dist‘(ℝ^‘𝑋)) |
146 | 135, 142,
143, 144, 145 | rrnprjdstle 40521 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → (abs‘((𝐹‘𝑖) − (𝑔‘𝑖))) ≤ (𝐹(dist‘(ℝ^‘𝑋))𝑔)) |
147 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(ℝ^‘𝑋) =
(ℝ^‘𝑋) |
148 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (ℝ
↑𝑚 𝑋) = (ℝ ↑𝑚
𝑋) |
149 | 147, 148 | rrxdsfi 40505 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑋 ∈ Fin →
(dist‘(ℝ^‘𝑋)) = (𝑓 ∈ (ℝ ↑𝑚
𝑋), 𝑔 ∈ (ℝ ↑𝑚
𝑋) ↦
(√‘Σ𝑘
∈ 𝑋 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)))) |
150 | 1, 149 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
(dist‘(ℝ^‘𝑋)) = (𝑓 ∈ (ℝ ↑𝑚
𝑋), 𝑔 ∈ (ℝ ↑𝑚
𝑋) ↦
(√‘Σ𝑘
∈ 𝑋 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)))) |
151 | 150, 69 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
(dist‘(ℝ^‘𝑋)) = 𝐷) |
152 | 151 | oveqd 6667 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐹(dist‘(ℝ^‘𝑋))𝑔) = (𝐹𝐷𝑔)) |
153 | 152 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → (𝐹(dist‘(ℝ^‘𝑋))𝑔) = (𝐹𝐷𝑔)) |
154 | 146, 153 | breqtrd 4679 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → (abs‘((𝐹‘𝑖) − (𝑔‘𝑖))) ≤ (𝐹𝐷𝑔)) |
155 | 121, 133,
128, 134, 154 | letrd 10194 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) − (𝑔‘𝑖)) ≤ (𝐹𝐷𝑔)) |
156 | 155 | 3adantl3 1219 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) − (𝑔‘𝑖)) ≤ (𝐹𝐷𝑔)) |
157 | | simpl3 1066 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → (𝐹𝐷𝑔) < 𝐸) |
158 | 122, 129,
131, 156, 157 | lelttrd 10195 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) − (𝑔‘𝑖)) < 𝐸) |
159 | | ltsub23 10508 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑖) ∈ ℝ ∧ (𝑔‘𝑖) ∈ ℝ ∧ 𝐸 ∈ ℝ) → (((𝐹‘𝑖) − (𝑔‘𝑖)) < 𝐸 ↔ ((𝐹‘𝑖) − 𝐸) < (𝑔‘𝑖))) |
160 | 119, 120,
130, 159 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → (((𝐹‘𝑖) − (𝑔‘𝑖)) < 𝐸 ↔ ((𝐹‘𝑖) − 𝐸) < (𝑔‘𝑖))) |
161 | 160 | 3adantl3 1219 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → (((𝐹‘𝑖) − (𝑔‘𝑖)) < 𝐸 ↔ ((𝐹‘𝑖) − 𝐸) < (𝑔‘𝑖))) |
162 | 158, 161 | mpbid 222 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) − 𝐸) < (𝑔‘𝑖)) |
163 | 92, 96, 91, 118, 162 | lelttrd 10195 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) < (𝑔‘𝑖)) |
164 | 21, 94 | readdcld 10069 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) + 𝐸) ∈ ℝ) |
165 | 164 | 3ad2antl1 1223 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) + 𝐸) ∈ ℝ) |
166 | 16 | 3ad2antl1 1223 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈ ℝ) |
167 | 120, 119 | resubcld 10458 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → ((𝑔‘𝑖) − (𝐹‘𝑖)) ∈ ℝ) |
168 | 167 | 3adantl3 1219 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → ((𝑔‘𝑖) − (𝐹‘𝑖)) ∈ ℝ) |
169 | 167 | leabsd 14153 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → ((𝑔‘𝑖) − (𝐹‘𝑖)) ≤ (abs‘((𝑔‘𝑖) − (𝐹‘𝑖)))) |
170 | 120 | recnd 10068 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → (𝑔‘𝑖) ∈ ℂ) |
171 | 119 | recnd 10068 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) ∈ ℂ) |
172 | 170, 171 | abssubd 14192 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → (abs‘((𝑔‘𝑖) − (𝐹‘𝑖))) = (abs‘((𝐹‘𝑖) − (𝑔‘𝑖)))) |
173 | 169, 172 | breqtrd 4679 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → ((𝑔‘𝑖) − (𝐹‘𝑖)) ≤ (abs‘((𝐹‘𝑖) − (𝑔‘𝑖)))) |
174 | 167, 133,
128, 173, 154 | letrd 10194 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → ((𝑔‘𝑖) − (𝐹‘𝑖)) ≤ (𝐹𝐷𝑔)) |
175 | 174 | 3adantl3 1219 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → ((𝑔‘𝑖) − (𝐹‘𝑖)) ≤ (𝐹𝐷𝑔)) |
176 | 168, 129,
131, 175, 157 | lelttrd 10195 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → ((𝑔‘𝑖) − (𝐹‘𝑖)) < 𝐸) |
177 | 119 | 3adantl3 1219 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) ∈ ℝ) |
178 | 91, 177, 131 | ltsubadd2d 10625 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → (((𝑔‘𝑖) − (𝐹‘𝑖)) < 𝐸 ↔ (𝑔‘𝑖) < ((𝐹‘𝑖) + 𝐸))) |
179 | 176, 178 | mpbid 222 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → (𝑔‘𝑖) < ((𝐹‘𝑖) + 𝐸)) |
180 | | min1 12020 |
. . . . . . . . . . . . . 14
⊢ ((((𝐵‘𝑖) − (𝐹‘𝑖)) ∈ ℝ ∧ ((𝐹‘𝑖) − (𝐴‘𝑖)) ∈ ℝ) → if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))) ≤ ((𝐵‘𝑖) − (𝐹‘𝑖))) |
181 | 22, 32, 180 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖))) ≤ ((𝐵‘𝑖) − (𝐹‘𝑖))) |
182 | 94, 97, 22, 113, 181 | letrd 10194 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝐸 ≤ ((𝐵‘𝑖) − (𝐹‘𝑖))) |
183 | 21, 94, 16 | leaddsub2d 10629 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (((𝐹‘𝑖) + 𝐸) ≤ (𝐵‘𝑖) ↔ 𝐸 ≤ ((𝐵‘𝑖) − (𝐹‘𝑖)))) |
184 | 182, 183 | mpbird 247 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) + 𝐸) ≤ (𝐵‘𝑖)) |
185 | 184 | 3ad2antl1 1223 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) + 𝐸) ≤ (𝐵‘𝑖)) |
186 | 91, 165, 166, 179, 185 | ltletrd 10197 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → (𝑔‘𝑖) < (𝐵‘𝑖)) |
187 | 83, 84, 91, 163, 186 | eliood 39720 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖 ∈ 𝑋) → (𝑔‘𝑖) ∈ ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
188 | 187 | ralrimiva 2966 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) → ∀𝑖 ∈ 𝑋 (𝑔‘𝑖) ∈ ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
189 | 82, 188 | jca 554 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) → (𝑔 Fn 𝑋 ∧ ∀𝑖 ∈ 𝑋 (𝑔‘𝑖) ∈ ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) |
190 | | vex 3203 |
. . . . . . 7
⊢ 𝑔 ∈ V |
191 | 190 | elixp 7915 |
. . . . . 6
⊢ (𝑔 ∈ X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ↔ (𝑔 Fn 𝑋 ∧ ∀𝑖 ∈ 𝑋 (𝑔‘𝑖) ∈ ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) |
192 | 189, 191 | sylibr 224 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ (ℝ ↑𝑚
𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) → 𝑔 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
193 | 80, 75, 11, 61, 192 | ballss3 39270 |
. . . 4
⊢ (𝜑 → (𝐹(ball‘𝐷)𝐸) ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
194 | 66, 193 | eqsstrd 3639 |
. . 3
⊢ (𝜑 → 𝑉 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
195 | 79, 194 | jca 554 |
. 2
⊢ (𝜑 → (𝐹 ∈ 𝑉 ∧ 𝑉 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) |
196 | | eleq2 2690 |
. . . 4
⊢ (𝑣 = 𝑉 → (𝐹 ∈ 𝑣 ↔ 𝐹 ∈ 𝑉)) |
197 | | sseq1 3626 |
. . . 4
⊢ (𝑣 = 𝑉 → (𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ↔ 𝑉 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) |
198 | 196, 197 | anbi12d 747 |
. . 3
⊢ (𝑣 = 𝑉 → ((𝐹 ∈ 𝑣 ∧ 𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) ↔ (𝐹 ∈ 𝑉 ∧ 𝑉 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))))) |
199 | 198 | rspcev 3309 |
. 2
⊢ ((𝑉 ∈
(TopOpen‘(ℝ^‘𝑋)) ∧ (𝐹 ∈ 𝑉 ∧ 𝑉 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) → ∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝐹 ∈ 𝑣 ∧ 𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) |
200 | 73, 195, 199 | syl2anc 693 |
1
⊢ (𝜑 → ∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝐹 ∈ 𝑣 ∧ 𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) |