Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ioorrnopnlem Structured version   Visualization version   GIF version

Theorem ioorrnopnlem 45597
Description: The a point in an indexed product of open intervals is contained in an open ball that is contained in the indexed product of open intervals. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
Hypotheses
Ref Expression
ioorrnopnlem.x (𝜑𝑋 ∈ Fin)
ioorrnopnlem.n (𝜑𝑋 ≠ ∅)
ioorrnopnlem.a (𝜑𝐴:𝑋⟶ℝ)
ioorrnopnlem.b (𝜑𝐵:𝑋⟶ℝ)
ioorrnopnlem.f (𝜑𝐹X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))
ioorrnopnlem.h 𝐻 = ran (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))))
ioorrnopnlem.e 𝐸 = inf(𝐻, ℝ, < )
ioorrnopnlem.v 𝑉 = (𝐹(ball‘𝐷)𝐸)
ioorrnopnlem.d 𝐷 = (𝑓 ∈ (ℝ ↑m 𝑋), 𝑔 ∈ (ℝ ↑m 𝑋) ↦ (√‘Σ𝑘𝑋 (((𝑓𝑘) − (𝑔𝑘))↑2)))
Assertion
Ref Expression
ioorrnopnlem (𝜑 → ∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝐹𝑣𝑣X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖))))
Distinct variable groups:   𝐴,𝑔   𝑣,𝐴   𝐵,𝑔   𝑣,𝐵   𝐷,𝑔,𝑖   𝑔,𝐸,𝑖   𝑔,𝐹,𝑖   𝑣,𝐹,𝑖   𝑣,𝑉   𝑓,𝑋,𝑔,𝑘   𝑖,𝑋,𝑣   𝜑,𝑓,𝑔,𝑘   𝜑,𝑖
Allowed substitution hints:   𝜑(𝑣)   𝐴(𝑓,𝑖,𝑘)   𝐵(𝑓,𝑖,𝑘)   𝐷(𝑣,𝑓,𝑘)   𝐸(𝑣,𝑓,𝑘)   𝐹(𝑓,𝑘)   𝐻(𝑣,𝑓,𝑔,𝑖,𝑘)   𝑉(𝑓,𝑔,𝑖,𝑘)

Proof of Theorem ioorrnopnlem
StepHypRef Expression
1 ioorrnopnlem.x . . . . 5 (𝜑𝑋 ∈ Fin)
2 ioorrnopnlem.d . . . . 5 𝐷 = (𝑓 ∈ (ℝ ↑m 𝑋), 𝑔 ∈ (ℝ ↑m 𝑋) ↦ (√‘Σ𝑘𝑋 (((𝑓𝑘) − (𝑔𝑘))↑2)))
31, 2rrndsxmet 45596 . . . 4 (𝜑𝐷 ∈ (∞Met‘(ℝ ↑m 𝑋)))
4 nfv 1909 . . . . . 6 𝑖𝜑
5 reex 11203 . . . . . . 7 ℝ ∈ V
65a1i 11 . . . . . 6 (𝜑 → ℝ ∈ V)
7 ioossre 13391 . . . . . . 7 ((𝐴𝑖)(,)(𝐵𝑖)) ⊆ ℝ
87a1i 11 . . . . . 6 ((𝜑𝑖𝑋) → ((𝐴𝑖)(,)(𝐵𝑖)) ⊆ ℝ)
94, 6, 8ixpssmapc 44341 . . . . 5 (𝜑X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)) ⊆ (ℝ ↑m 𝑋))
10 ioorrnopnlem.f . . . . 5 (𝜑𝐹X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))
119, 10sseldd 3978 . . . 4 (𝜑𝐹 ∈ (ℝ ↑m 𝑋))
12 ioorrnopnlem.e . . . . . 6 𝐸 = inf(𝐻, ℝ, < )
13 ioorrnopnlem.h . . . . . . . . 9 𝐻 = ran (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))))
1413a1i 11 . . . . . . . 8 (𝜑𝐻 = ran (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖)))))
15 ioorrnopnlem.b . . . . . . . . . . . . . 14 (𝜑𝐵:𝑋⟶ℝ)
1615ffvelcdmda 7080 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → (𝐵𝑖) ∈ ℝ)
1710adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑋) → 𝐹X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))
18 simpr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑋) → 𝑖𝑋)
19 fvixp2 44475 . . . . . . . . . . . . . . 15 ((𝐹X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)) ∧ 𝑖𝑋) → (𝐹𝑖) ∈ ((𝐴𝑖)(,)(𝐵𝑖)))
2017, 18, 19syl2anc 583 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋) → (𝐹𝑖) ∈ ((𝐴𝑖)(,)(𝐵𝑖)))
217, 20sselid 3975 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → (𝐹𝑖) ∈ ℝ)
2216, 21resubcld 11646 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → ((𝐵𝑖) − (𝐹𝑖)) ∈ ℝ)
23 ioorrnopnlem.a . . . . . . . . . . . . . . . 16 (𝜑𝐴:𝑋⟶ℝ)
2423ffvelcdmda 7080 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑋) → (𝐴𝑖) ∈ ℝ)
2524rexrd 11268 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋) → (𝐴𝑖) ∈ ℝ*)
2616rexrd 11268 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋) → (𝐵𝑖) ∈ ℝ*)
27 iooltub 44800 . . . . . . . . . . . . . 14 (((𝐴𝑖) ∈ ℝ* ∧ (𝐵𝑖) ∈ ℝ* ∧ (𝐹𝑖) ∈ ((𝐴𝑖)(,)(𝐵𝑖))) → (𝐹𝑖) < (𝐵𝑖))
2825, 26, 20, 27syl3anc 1368 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → (𝐹𝑖) < (𝐵𝑖))
2921, 16posdifd 11805 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → ((𝐹𝑖) < (𝐵𝑖) ↔ 0 < ((𝐵𝑖) − (𝐹𝑖))))
3028, 29mpbid 231 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → 0 < ((𝐵𝑖) − (𝐹𝑖)))
3122, 30elrpd 13019 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → ((𝐵𝑖) − (𝐹𝑖)) ∈ ℝ+)
3221, 24resubcld 11646 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → ((𝐹𝑖) − (𝐴𝑖)) ∈ ℝ)
33 ioogtlb 44785 . . . . . . . . . . . . . 14 (((𝐴𝑖) ∈ ℝ* ∧ (𝐵𝑖) ∈ ℝ* ∧ (𝐹𝑖) ∈ ((𝐴𝑖)(,)(𝐵𝑖))) → (𝐴𝑖) < (𝐹𝑖))
3425, 26, 20, 33syl3anc 1368 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → (𝐴𝑖) < (𝐹𝑖))
3524, 21posdifd 11805 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → ((𝐴𝑖) < (𝐹𝑖) ↔ 0 < ((𝐹𝑖) − (𝐴𝑖))))
3634, 35mpbid 231 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → 0 < ((𝐹𝑖) − (𝐴𝑖)))
3732, 36elrpd 13019 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → ((𝐹𝑖) − (𝐴𝑖)) ∈ ℝ+)
3831, 37ifcld 4569 . . . . . . . . . 10 ((𝜑𝑖𝑋) → if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ∈ ℝ+)
3938ralrimiva 3140 . . . . . . . . 9 (𝜑 → ∀𝑖𝑋 if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ∈ ℝ+)
40 eqid 2726 . . . . . . . . . 10 (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖)))) = (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))))
4140rnmptss 7118 . . . . . . . . 9 (∀𝑖𝑋 if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ∈ ℝ+ → ran (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖)))) ⊆ ℝ+)
4239, 41syl 17 . . . . . . . 8 (𝜑 → ran (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖)))) ⊆ ℝ+)
4314, 42eqsstrd 4015 . . . . . . 7 (𝜑𝐻 ⊆ ℝ+)
44 ltso 11298 . . . . . . . . 9 < Or ℝ
4544a1i 11 . . . . . . . 8 (𝜑 → < Or ℝ)
4640rnmptfi 44447 . . . . . . . . . 10 (𝑋 ∈ Fin → ran (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖)))) ∈ Fin)
471, 46syl 17 . . . . . . . . 9 (𝜑 → ran (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖)))) ∈ Fin)
4813, 47eqeltrid 2831 . . . . . . . 8 (𝜑𝐻 ∈ Fin)
49 ioorrnopnlem.n . . . . . . . . . 10 (𝜑𝑋 ≠ ∅)
504, 38, 40, 49rnmptn0 6237 . . . . . . . . 9 (𝜑 → ran (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖)))) ≠ ∅)
5114, 50eqnetrd 3002 . . . . . . . 8 (𝜑𝐻 ≠ ∅)
52 rpssre 12987 . . . . . . . . . 10 + ⊆ ℝ
5352a1i 11 . . . . . . . . 9 (𝜑 → ℝ+ ⊆ ℝ)
5443, 53sstrd 3987 . . . . . . . 8 (𝜑𝐻 ⊆ ℝ)
55 fiinfcl 9498 . . . . . . . 8 (( < Or ℝ ∧ (𝐻 ∈ Fin ∧ 𝐻 ≠ ∅ ∧ 𝐻 ⊆ ℝ)) → inf(𝐻, ℝ, < ) ∈ 𝐻)
5645, 48, 51, 54, 55syl13anc 1369 . . . . . . 7 (𝜑 → inf(𝐻, ℝ, < ) ∈ 𝐻)
5743, 56sseldd 3978 . . . . . 6 (𝜑 → inf(𝐻, ℝ, < ) ∈ ℝ+)
5812, 57eqeltrid 2831 . . . . 5 (𝜑𝐸 ∈ ℝ+)
59 rpxr 12989 . . . . 5 (𝐸 ∈ ℝ+𝐸 ∈ ℝ*)
6058, 59syl 17 . . . 4 (𝜑𝐸 ∈ ℝ*)
61 eqid 2726 . . . . 5 (MetOpen‘𝐷) = (MetOpen‘𝐷)
6261blopn 24364 . . . 4 ((𝐷 ∈ (∞Met‘(ℝ ↑m 𝑋)) ∧ 𝐹 ∈ (ℝ ↑m 𝑋) ∧ 𝐸 ∈ ℝ*) → (𝐹(ball‘𝐷)𝐸) ∈ (MetOpen‘𝐷))
633, 11, 60, 62syl3anc 1368 . . 3 (𝜑 → (𝐹(ball‘𝐷)𝐸) ∈ (MetOpen‘𝐷))
64 ioorrnopnlem.v . . . . 5 𝑉 = (𝐹(ball‘𝐷)𝐸)
6564a1i 11 . . . 4 (𝜑𝑉 = (𝐹(ball‘𝐷)𝐸))
661rrxtopnfi 45580 . . . . 5 (𝜑 → (TopOpen‘(ℝ^‘𝑋)) = (MetOpen‘(𝑓 ∈ (ℝ ↑m 𝑋), 𝑔 ∈ (ℝ ↑m 𝑋) ↦ (√‘Σ𝑘𝑋 (((𝑓𝑘) − (𝑔𝑘))↑2)))))
672eqcomi 2735 . . . . . . 7 (𝑓 ∈ (ℝ ↑m 𝑋), 𝑔 ∈ (ℝ ↑m 𝑋) ↦ (√‘Σ𝑘𝑋 (((𝑓𝑘) − (𝑔𝑘))↑2))) = 𝐷
6867a1i 11 . . . . . 6 (𝜑 → (𝑓 ∈ (ℝ ↑m 𝑋), 𝑔 ∈ (ℝ ↑m 𝑋) ↦ (√‘Σ𝑘𝑋 (((𝑓𝑘) − (𝑔𝑘))↑2))) = 𝐷)
6968fveq2d 6889 . . . . 5 (𝜑 → (MetOpen‘(𝑓 ∈ (ℝ ↑m 𝑋), 𝑔 ∈ (ℝ ↑m 𝑋) ↦ (√‘Σ𝑘𝑋 (((𝑓𝑘) − (𝑔𝑘))↑2)))) = (MetOpen‘𝐷))
7066, 69eqtrd 2766 . . . 4 (𝜑 → (TopOpen‘(ℝ^‘𝑋)) = (MetOpen‘𝐷))
7165, 70eleq12d 2821 . . 3 (𝜑 → (𝑉 ∈ (TopOpen‘(ℝ^‘𝑋)) ↔ (𝐹(ball‘𝐷)𝐸) ∈ (MetOpen‘𝐷)))
7263, 71mpbird 257 . 2 (𝜑𝑉 ∈ (TopOpen‘(ℝ^‘𝑋)))
73 xmetpsmet 24209 . . . . . 6 (𝐷 ∈ (∞Met‘(ℝ ↑m 𝑋)) → 𝐷 ∈ (PsMet‘(ℝ ↑m 𝑋)))
743, 73syl 17 . . . . 5 (𝜑𝐷 ∈ (PsMet‘(ℝ ↑m 𝑋)))
75 blcntrps 24273 . . . . 5 ((𝐷 ∈ (PsMet‘(ℝ ↑m 𝑋)) ∧ 𝐹 ∈ (ℝ ↑m 𝑋) ∧ 𝐸 ∈ ℝ+) → 𝐹 ∈ (𝐹(ball‘𝐷)𝐸))
7674, 11, 58, 75syl3anc 1368 . . . 4 (𝜑𝐹 ∈ (𝐹(ball‘𝐷)𝐸))
7765eqcomd 2732 . . . 4 (𝜑 → (𝐹(ball‘𝐷)𝐸) = 𝑉)
7876, 77eleqtrd 2829 . . 3 (𝜑𝐹𝑉)
79 nfv 1909 . . . . 5 𝑔𝜑
80 elmapfn 8861 . . . . . . . 8 (𝑔 ∈ (ℝ ↑m 𝑋) → 𝑔 Fn 𝑋)
81803ad2ant2 1131 . . . . . . 7 ((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) → 𝑔 Fn 𝑋)
82253ad2antl1 1182 . . . . . . . . 9 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝐴𝑖) ∈ ℝ*)
83263ad2antl1 1182 . . . . . . . . 9 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝐵𝑖) ∈ ℝ*)
84 simpl2 1189 . . . . . . . . . 10 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → 𝑔 ∈ (ℝ ↑m 𝑋))
85 simpr 484 . . . . . . . . . 10 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → 𝑖𝑋)
86 elmapi 8845 . . . . . . . . . . . 12 (𝑔 ∈ (ℝ ↑m 𝑋) → 𝑔:𝑋⟶ℝ)
8786adantr 480 . . . . . . . . . . 11 ((𝑔 ∈ (ℝ ↑m 𝑋) ∧ 𝑖𝑋) → 𝑔:𝑋⟶ℝ)
88 simpr 484 . . . . . . . . . . 11 ((𝑔 ∈ (ℝ ↑m 𝑋) ∧ 𝑖𝑋) → 𝑖𝑋)
8987, 88ffvelcdmd 7081 . . . . . . . . . 10 ((𝑔 ∈ (ℝ ↑m 𝑋) ∧ 𝑖𝑋) → (𝑔𝑖) ∈ ℝ)
9084, 85, 89syl2anc 583 . . . . . . . . 9 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝑔𝑖) ∈ ℝ)
91243ad2antl1 1182 . . . . . . . . . 10 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝐴𝑖) ∈ ℝ)
9252, 58sselid 3975 . . . . . . . . . . . . 13 (𝜑𝐸 ∈ ℝ)
9392adantr 480 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → 𝐸 ∈ ℝ)
9421, 93resubcld 11646 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → ((𝐹𝑖) − 𝐸) ∈ ℝ)
95943ad2antl1 1182 . . . . . . . . . 10 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → ((𝐹𝑖) − 𝐸) ∈ ℝ)
9652, 38sselid 3975 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ∈ ℝ)
9712a1i 11 . . . . . . . . . . . . . . . 16 (𝜑𝐸 = inf(𝐻, ℝ, < ))
98 infxrrefi 44669 . . . . . . . . . . . . . . . . . 18 ((𝐻 ⊆ ℝ ∧ 𝐻 ∈ Fin ∧ 𝐻 ≠ ∅) → inf(𝐻, ℝ*, < ) = inf(𝐻, ℝ, < ))
9954, 48, 51, 98syl3anc 1368 . . . . . . . . . . . . . . . . 17 (𝜑 → inf(𝐻, ℝ*, < ) = inf(𝐻, ℝ, < ))
10099eqcomd 2732 . . . . . . . . . . . . . . . 16 (𝜑 → inf(𝐻, ℝ, < ) = inf(𝐻, ℝ*, < ))
10197, 100eqtrd 2766 . . . . . . . . . . . . . . 15 (𝜑𝐸 = inf(𝐻, ℝ*, < ))
102101adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋) → 𝐸 = inf(𝐻, ℝ*, < ))
103 ressxr 11262 . . . . . . . . . . . . . . . . . 18 ℝ ⊆ ℝ*
104103a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → ℝ ⊆ ℝ*)
10554, 104sstrd 3987 . . . . . . . . . . . . . . . 16 (𝜑𝐻 ⊆ ℝ*)
106105adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑋) → 𝐻 ⊆ ℝ*)
10738elexd 3489 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖𝑋) → if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ∈ V)
10840elrnmpt1 5951 . . . . . . . . . . . . . . . . 17 ((𝑖𝑋 ∧ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ∈ V) → if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ∈ ran (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖)))))
10918, 107, 108syl2anc 583 . . . . . . . . . . . . . . . 16 ((𝜑𝑖𝑋) → if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ∈ ran (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖)))))
110109, 13eleqtrrdi 2838 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑋) → if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ∈ 𝐻)
111 infxrlb 13319 . . . . . . . . . . . . . . 15 ((𝐻 ⊆ ℝ* ∧ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ∈ 𝐻) → inf(𝐻, ℝ*, < ) ≤ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))))
112106, 110, 111syl2anc 583 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋) → inf(𝐻, ℝ*, < ) ≤ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))))
113102, 112eqbrtrd 5163 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → 𝐸 ≤ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))))
114 min2 13175 . . . . . . . . . . . . . 14 ((((𝐵𝑖) − (𝐹𝑖)) ∈ ℝ ∧ ((𝐹𝑖) − (𝐴𝑖)) ∈ ℝ) → if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ≤ ((𝐹𝑖) − (𝐴𝑖)))
11522, 32, 114syl2anc 583 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ≤ ((𝐹𝑖) − (𝐴𝑖)))
11693, 96, 32, 113, 115letrd 11375 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → 𝐸 ≤ ((𝐹𝑖) − (𝐴𝑖)))
11793, 21, 24, 116lesubd 11822 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → (𝐴𝑖) ≤ ((𝐹𝑖) − 𝐸))
1181173ad2antl1 1182 . . . . . . . . . 10 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝐴𝑖) ≤ ((𝐹𝑖) − 𝐸))
11921adantlr 712 . . . . . . . . . . . . . 14 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → (𝐹𝑖) ∈ ℝ)
12089adantll 711 . . . . . . . . . . . . . 14 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → (𝑔𝑖) ∈ ℝ)
121119, 120resubcld 11646 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → ((𝐹𝑖) − (𝑔𝑖)) ∈ ℝ)
1221213adantl3 1165 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → ((𝐹𝑖) − (𝑔𝑖)) ∈ ℝ)
1231, 2rrndsmet 45595 . . . . . . . . . . . . . . 15 (𝜑𝐷 ∈ (Met‘(ℝ ↑m 𝑋)))
124123ad2antrr 723 . . . . . . . . . . . . . 14 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → 𝐷 ∈ (Met‘(ℝ ↑m 𝑋)))
12511ad2antrr 723 . . . . . . . . . . . . . 14 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → 𝐹 ∈ (ℝ ↑m 𝑋))
126 simplr 766 . . . . . . . . . . . . . 14 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → 𝑔 ∈ (ℝ ↑m 𝑋))
127 metcl 24193 . . . . . . . . . . . . . 14 ((𝐷 ∈ (Met‘(ℝ ↑m 𝑋)) ∧ 𝐹 ∈ (ℝ ↑m 𝑋) ∧ 𝑔 ∈ (ℝ ↑m 𝑋)) → (𝐹𝐷𝑔) ∈ ℝ)
128124, 125, 126, 127syl3anc 1368 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → (𝐹𝐷𝑔) ∈ ℝ)
1291283adantl3 1165 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝐹𝐷𝑔) ∈ ℝ)
13093adantlr 712 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → 𝐸 ∈ ℝ)
1311303adantl3 1165 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → 𝐸 ∈ ℝ)
132121recnd 11246 . . . . . . . . . . . . . . 15 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → ((𝐹𝑖) − (𝑔𝑖)) ∈ ℂ)
133132abscld 15389 . . . . . . . . . . . . . 14 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → (abs‘((𝐹𝑖) − (𝑔𝑖))) ∈ ℝ)
134121leabsd 15367 . . . . . . . . . . . . . 14 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → ((𝐹𝑖) − (𝑔𝑖)) ≤ (abs‘((𝐹𝑖) − (𝑔𝑖))))
1351ad2antrr 723 . . . . . . . . . . . . . . . 16 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → 𝑋 ∈ Fin)
136 ixpf 8916 . . . . . . . . . . . . . . . . . . 19 (𝐹X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)) → 𝐹:𝑋 𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))
13710, 136syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹:𝑋 𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))
1388ralrimiva 3140 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)) ⊆ ℝ)
139 iunss 5041 . . . . . . . . . . . . . . . . . . 19 ( 𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)) ⊆ ℝ ↔ ∀𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)) ⊆ ℝ)
140138, 139sylibr 233 . . . . . . . . . . . . . . . . . 18 (𝜑 𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)) ⊆ ℝ)
141137, 140fssd 6729 . . . . . . . . . . . . . . . . 17 (𝜑𝐹:𝑋⟶ℝ)
142141ad2antrr 723 . . . . . . . . . . . . . . . 16 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → 𝐹:𝑋⟶ℝ)
143126, 86syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → 𝑔:𝑋⟶ℝ)
144 simpr 484 . . . . . . . . . . . . . . . 16 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → 𝑖𝑋)
145 eqid 2726 . . . . . . . . . . . . . . . 16 (dist‘(ℝ^‘𝑋)) = (dist‘(ℝ^‘𝑋))
146135, 142, 143, 144, 145rrnprjdstle 45594 . . . . . . . . . . . . . . 15 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → (abs‘((𝐹𝑖) − (𝑔𝑖))) ≤ (𝐹(dist‘(ℝ^‘𝑋))𝑔))
147 eqid 2726 . . . . . . . . . . . . . . . . . . . 20 (ℝ^‘𝑋) = (ℝ^‘𝑋)
148 eqid 2726 . . . . . . . . . . . . . . . . . . . 20 (ℝ ↑m 𝑋) = (ℝ ↑m 𝑋)
149147, 148rrxdsfi 25294 . . . . . . . . . . . . . . . . . . 19 (𝑋 ∈ Fin → (dist‘(ℝ^‘𝑋)) = (𝑓 ∈ (ℝ ↑m 𝑋), 𝑔 ∈ (ℝ ↑m 𝑋) ↦ (√‘Σ𝑘𝑋 (((𝑓𝑘) − (𝑔𝑘))↑2))))
1501, 149syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (dist‘(ℝ^‘𝑋)) = (𝑓 ∈ (ℝ ↑m 𝑋), 𝑔 ∈ (ℝ ↑m 𝑋) ↦ (√‘Σ𝑘𝑋 (((𝑓𝑘) − (𝑔𝑘))↑2))))
151150, 68eqtrd 2766 . . . . . . . . . . . . . . . . 17 (𝜑 → (dist‘(ℝ^‘𝑋)) = 𝐷)
152151oveqd 7422 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹(dist‘(ℝ^‘𝑋))𝑔) = (𝐹𝐷𝑔))
153152ad2antrr 723 . . . . . . . . . . . . . . 15 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → (𝐹(dist‘(ℝ^‘𝑋))𝑔) = (𝐹𝐷𝑔))
154146, 153breqtrd 5167 . . . . . . . . . . . . . 14 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → (abs‘((𝐹𝑖) − (𝑔𝑖))) ≤ (𝐹𝐷𝑔))
155121, 133, 128, 134, 154letrd 11375 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → ((𝐹𝑖) − (𝑔𝑖)) ≤ (𝐹𝐷𝑔))
1561553adantl3 1165 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → ((𝐹𝑖) − (𝑔𝑖)) ≤ (𝐹𝐷𝑔))
157 simpl3 1190 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝐹𝐷𝑔) < 𝐸)
158122, 129, 131, 156, 157lelttrd 11376 . . . . . . . . . . 11 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → ((𝐹𝑖) − (𝑔𝑖)) < 𝐸)
159 ltsub23 11698 . . . . . . . . . . . . 13 (((𝐹𝑖) ∈ ℝ ∧ (𝑔𝑖) ∈ ℝ ∧ 𝐸 ∈ ℝ) → (((𝐹𝑖) − (𝑔𝑖)) < 𝐸 ↔ ((𝐹𝑖) − 𝐸) < (𝑔𝑖)))
160119, 120, 130, 159syl3anc 1368 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → (((𝐹𝑖) − (𝑔𝑖)) < 𝐸 ↔ ((𝐹𝑖) − 𝐸) < (𝑔𝑖)))
1611603adantl3 1165 . . . . . . . . . . 11 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (((𝐹𝑖) − (𝑔𝑖)) < 𝐸 ↔ ((𝐹𝑖) − 𝐸) < (𝑔𝑖)))
162158, 161mpbid 231 . . . . . . . . . 10 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → ((𝐹𝑖) − 𝐸) < (𝑔𝑖))
16391, 95, 90, 118, 162lelttrd 11376 . . . . . . . . 9 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝐴𝑖) < (𝑔𝑖))
16421, 93readdcld 11247 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → ((𝐹𝑖) + 𝐸) ∈ ℝ)
1651643ad2antl1 1182 . . . . . . . . . 10 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → ((𝐹𝑖) + 𝐸) ∈ ℝ)
166163ad2antl1 1182 . . . . . . . . . 10 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝐵𝑖) ∈ ℝ)
167120, 119resubcld 11646 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → ((𝑔𝑖) − (𝐹𝑖)) ∈ ℝ)
1681673adantl3 1165 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → ((𝑔𝑖) − (𝐹𝑖)) ∈ ℝ)
169167leabsd 15367 . . . . . . . . . . . . . . 15 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → ((𝑔𝑖) − (𝐹𝑖)) ≤ (abs‘((𝑔𝑖) − (𝐹𝑖))))
170120recnd 11246 . . . . . . . . . . . . . . . 16 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → (𝑔𝑖) ∈ ℂ)
171119recnd 11246 . . . . . . . . . . . . . . . 16 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → (𝐹𝑖) ∈ ℂ)
172170, 171abssubd 15406 . . . . . . . . . . . . . . 15 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → (abs‘((𝑔𝑖) − (𝐹𝑖))) = (abs‘((𝐹𝑖) − (𝑔𝑖))))
173169, 172breqtrd 5167 . . . . . . . . . . . . . 14 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → ((𝑔𝑖) − (𝐹𝑖)) ≤ (abs‘((𝐹𝑖) − (𝑔𝑖))))
174167, 133, 128, 173, 154letrd 11375 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → ((𝑔𝑖) − (𝐹𝑖)) ≤ (𝐹𝐷𝑔))
1751743adantl3 1165 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → ((𝑔𝑖) − (𝐹𝑖)) ≤ (𝐹𝐷𝑔))
176168, 129, 131, 175, 157lelttrd 11376 . . . . . . . . . . 11 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → ((𝑔𝑖) − (𝐹𝑖)) < 𝐸)
1771193adantl3 1165 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝐹𝑖) ∈ ℝ)
17890, 177, 131ltsubadd2d 11816 . . . . . . . . . . 11 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (((𝑔𝑖) − (𝐹𝑖)) < 𝐸 ↔ (𝑔𝑖) < ((𝐹𝑖) + 𝐸)))
179176, 178mpbid 231 . . . . . . . . . 10 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝑔𝑖) < ((𝐹𝑖) + 𝐸))
180 min1 13174 . . . . . . . . . . . . . 14 ((((𝐵𝑖) − (𝐹𝑖)) ∈ ℝ ∧ ((𝐹𝑖) − (𝐴𝑖)) ∈ ℝ) → if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ≤ ((𝐵𝑖) − (𝐹𝑖)))
18122, 32, 180syl2anc 583 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ≤ ((𝐵𝑖) − (𝐹𝑖)))
18293, 96, 22, 113, 181letrd 11375 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → 𝐸 ≤ ((𝐵𝑖) − (𝐹𝑖)))
18321, 93, 16leaddsub2d 11820 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → (((𝐹𝑖) + 𝐸) ≤ (𝐵𝑖) ↔ 𝐸 ≤ ((𝐵𝑖) − (𝐹𝑖))))
184182, 183mpbird 257 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → ((𝐹𝑖) + 𝐸) ≤ (𝐵𝑖))
1851843ad2antl1 1182 . . . . . . . . . 10 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → ((𝐹𝑖) + 𝐸) ≤ (𝐵𝑖))
18690, 165, 166, 179, 185ltletrd 11378 . . . . . . . . 9 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝑔𝑖) < (𝐵𝑖))
18782, 83, 90, 163, 186eliood 44788 . . . . . . . 8 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝑔𝑖) ∈ ((𝐴𝑖)(,)(𝐵𝑖)))
188187ralrimiva 3140 . . . . . . 7 ((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) → ∀𝑖𝑋 (𝑔𝑖) ∈ ((𝐴𝑖)(,)(𝐵𝑖)))
18981, 188jca 511 . . . . . 6 ((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) → (𝑔 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑔𝑖) ∈ ((𝐴𝑖)(,)(𝐵𝑖))))
190 vex 3472 . . . . . . 7 𝑔 ∈ V
191190elixp 8900 . . . . . 6 (𝑔X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)) ↔ (𝑔 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑔𝑖) ∈ ((𝐴𝑖)(,)(𝐵𝑖))))
192189, 191sylibr 233 . . . . 5 ((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) → 𝑔X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))
19379, 74, 11, 60, 192ballss3 44362 . . . 4 (𝜑 → (𝐹(ball‘𝐷)𝐸) ⊆ X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))
19465, 193eqsstrd 4015 . . 3 (𝜑𝑉X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))
19578, 194jca 511 . 2 (𝜑 → (𝐹𝑉𝑉X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖))))
196 eleq2 2816 . . . 4 (𝑣 = 𝑉 → (𝐹𝑣𝐹𝑉))
197 sseq1 4002 . . . 4 (𝑣 = 𝑉 → (𝑣X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)) ↔ 𝑉X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖))))
198196, 197anbi12d 630 . . 3 (𝑣 = 𝑉 → ((𝐹𝑣𝑣X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖))) ↔ (𝐹𝑉𝑉X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))))
199198rspcev 3606 . 2 ((𝑉 ∈ (TopOpen‘(ℝ^‘𝑋)) ∧ (𝐹𝑉𝑉X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))) → ∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝐹𝑣𝑣X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖))))
20072, 195, 199syl2anc 583 1 (𝜑 → ∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝐹𝑣𝑣X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3a 1084   = wceq 1533  wcel 2098  wne 2934  wral 3055  wrex 3064  Vcvv 3468  wss 3943  c0 4317  ifcif 4523   ciun 4990   class class class wbr 5141  cmpt 5224   Or wor 5580  ran crn 5670   Fn wfn 6532  wf 6533  cfv 6537  (class class class)co 7405  cmpo 7407  m cmap 8822  Xcixp 8893  Fincfn 8941  infcinf 9438  cr 11111  0cc0 11112   + caddc 11115  *cxr 11251   < clt 11252  cle 11253  cmin 11448  2c2 12271  +crp 12980  (,)cioo 13330  cexp 14032  csqrt 15186  abscabs 15187  Σcsu 15638  distcds 17215  TopOpenctopn 17376  PsMetcpsmet 21224  ∞Metcxmet 21225  Metcmet 21226  ballcbl 21227  MetOpencmopn 21230  ℝ^crrx 25266
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190  ax-addf 11191  ax-mulf 11192
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-se 5625  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7667  df-om 7853  df-1st 7974  df-2nd 7975  df-supp 8147  df-tpos 8212  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-1o 8467  df-er 8705  df-map 8824  df-ixp 8894  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9364  df-sup 9439  df-inf 9440  df-oi 9507  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-4 12281  df-5 12282  df-6 12283  df-7 12284  df-8 12285  df-9 12286  df-n0 12477  df-z 12563  df-dec 12682  df-uz 12827  df-q 12937  df-rp 12981  df-xneg 13098  df-xadd 13099  df-xmul 13100  df-ioo 13334  df-ico 13336  df-fz 13491  df-fzo 13634  df-seq 13973  df-exp 14033  df-hash 14296  df-cj 15052  df-re 15053  df-im 15054  df-sqrt 15188  df-abs 15189  df-clim 15438  df-sum 15639  df-struct 17089  df-sets 17106  df-slot 17124  df-ndx 17136  df-base 17154  df-ress 17183  df-plusg 17219  df-mulr 17220  df-starv 17221  df-sca 17222  df-vsca 17223  df-ip 17224  df-tset 17225  df-ple 17226  df-ds 17228  df-unif 17229  df-hom 17230  df-cco 17231  df-rest 17377  df-topn 17378  df-0g 17396  df-gsum 17397  df-topgen 17398  df-prds 17402  df-pws 17404  df-mgm 18573  df-sgrp 18652  df-mnd 18668  df-mhm 18713  df-grp 18866  df-minusg 18867  df-sbg 18868  df-subg 19050  df-ghm 19139  df-cntz 19233  df-cmn 19702  df-abl 19703  df-mgp 20040  df-rng 20058  df-ur 20087  df-ring 20140  df-cring 20141  df-oppr 20236  df-dvdsr 20259  df-unit 20260  df-invr 20290  df-dvr 20303  df-rhm 20374  df-subrng 20446  df-subrg 20471  df-drng 20589  df-field 20590  df-staf 20688  df-srng 20689  df-lmod 20708  df-lss 20779  df-sra 21021  df-rgmod 21022  df-psmet 21232  df-xmet 21233  df-met 21234  df-bl 21235  df-mopn 21236  df-cnfld 21241  df-refld 21498  df-dsmm 21627  df-frlm 21642  df-top 22751  df-topon 22768  df-bases 22804  df-nm 24446  df-tng 24448  df-tcph 25052  df-rrx 25268
This theorem is referenced by:  ioorrnopn  45598
  Copyright terms: Public domain W3C validator