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 42788
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 42787 . . . 4 (𝜑𝐷 ∈ (∞Met‘(ℝ ↑m 𝑋)))
4 nfv 1916 . . . . . 6 𝑖𝜑
5 reex 10613 . . . . . . 7 ℝ ∈ V
65a1i 11 . . . . . 6 (𝜑 → ℝ ∈ V)
7 ioossre 12784 . . . . . . 7 ((𝐴𝑖)(,)(𝐵𝑖)) ⊆ ℝ
87a1i 11 . . . . . 6 ((𝜑𝑖𝑋) → ((𝐴𝑖)(,)(𝐵𝑖)) ⊆ ℝ)
94, 6, 8ixpssmapc 41544 . . . . 5 (𝜑X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)) ⊆ (ℝ ↑m 𝑋))
10 ioorrnopnlem.f . . . . 5 (𝜑𝐹X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))
119, 10sseldd 3952 . . . 4 (𝜑𝐹 ∈ (ℝ ↑m 𝑋))
12 ioorrnopnlem.e . . . . . 6 𝐸 = inf(𝐻, ℝ, < )
13 ioorrnopnlem.h . . . . . . . . 9 𝐻 = ran (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))))
1413a1i 11 . . . . . . . 8 (𝜑𝐻 = ran (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖)))))
15 ioorrnopnlem.b . . . . . . . . . . . . . 14 (𝜑𝐵:𝑋⟶ℝ)
1615ffvelrnda 6832 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → (𝐵𝑖) ∈ ℝ)
1710adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑋) → 𝐹X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))
18 simpr 488 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑋) → 𝑖𝑋)
19 fvixp2 41668 . . . . . . . . . . . . . . 15 ((𝐹X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)) ∧ 𝑖𝑋) → (𝐹𝑖) ∈ ((𝐴𝑖)(,)(𝐵𝑖)))
2017, 18, 19syl2anc 587 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋) → (𝐹𝑖) ∈ ((𝐴𝑖)(,)(𝐵𝑖)))
217, 20sseldi 3949 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → (𝐹𝑖) ∈ ℝ)
2216, 21resubcld 11053 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → ((𝐵𝑖) − (𝐹𝑖)) ∈ ℝ)
23 ioorrnopnlem.a . . . . . . . . . . . . . . . 16 (𝜑𝐴:𝑋⟶ℝ)
2423ffvelrnda 6832 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑋) → (𝐴𝑖) ∈ ℝ)
2524rexrd 10676 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋) → (𝐴𝑖) ∈ ℝ*)
2616rexrd 10676 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋) → (𝐵𝑖) ∈ ℝ*)
27 iooltub 41989 . . . . . . . . . . . . . 14 (((𝐴𝑖) ∈ ℝ* ∧ (𝐵𝑖) ∈ ℝ* ∧ (𝐹𝑖) ∈ ((𝐴𝑖)(,)(𝐵𝑖))) → (𝐹𝑖) < (𝐵𝑖))
2825, 26, 20, 27syl3anc 1368 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → (𝐹𝑖) < (𝐵𝑖))
2921, 16posdifd 11212 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → ((𝐹𝑖) < (𝐵𝑖) ↔ 0 < ((𝐵𝑖) − (𝐹𝑖))))
3028, 29mpbid 235 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → 0 < ((𝐵𝑖) − (𝐹𝑖)))
3122, 30elrpd 12414 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → ((𝐵𝑖) − (𝐹𝑖)) ∈ ℝ+)
3221, 24resubcld 11053 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → ((𝐹𝑖) − (𝐴𝑖)) ∈ ℝ)
33 ioogtlb 41974 . . . . . . . . . . . . . 14 (((𝐴𝑖) ∈ ℝ* ∧ (𝐵𝑖) ∈ ℝ* ∧ (𝐹𝑖) ∈ ((𝐴𝑖)(,)(𝐵𝑖))) → (𝐴𝑖) < (𝐹𝑖))
3425, 26, 20, 33syl3anc 1368 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → (𝐴𝑖) < (𝐹𝑖))
3524, 21posdifd 11212 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → ((𝐴𝑖) < (𝐹𝑖) ↔ 0 < ((𝐹𝑖) − (𝐴𝑖))))
3634, 35mpbid 235 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → 0 < ((𝐹𝑖) − (𝐴𝑖)))
3732, 36elrpd 12414 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → ((𝐹𝑖) − (𝐴𝑖)) ∈ ℝ+)
3831, 37ifcld 4493 . . . . . . . . . 10 ((𝜑𝑖𝑋) → if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ∈ ℝ+)
3938ralrimiva 3176 . . . . . . . . 9 (𝜑 → ∀𝑖𝑋 if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ∈ ℝ+)
40 eqid 2824 . . . . . . . . . 10 (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖)))) = (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))))
4140rnmptss 6867 . . . . . . . . 9 (∀𝑖𝑋 if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ∈ ℝ+ → ran (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖)))) ⊆ ℝ+)
4239, 41syl 17 . . . . . . . 8 (𝜑 → ran (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖)))) ⊆ ℝ+)
4314, 42eqsstrd 3989 . . . . . . 7 (𝜑𝐻 ⊆ ℝ+)
44 ltso 10706 . . . . . . . . 9 < Or ℝ
4544a1i 11 . . . . . . . 8 (𝜑 → < Or ℝ)
4640rnmptfi 41634 . . . . . . . . . 10 (𝑋 ∈ Fin → ran (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖)))) ∈ Fin)
471, 46syl 17 . . . . . . . . 9 (𝜑 → ran (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖)))) ∈ Fin)
4813, 47eqeltrid 2920 . . . . . . . 8 (𝜑𝐻 ∈ Fin)
4938elexd 3499 . . . . . . . . . 10 ((𝜑𝑖𝑋) → if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ∈ V)
50 ioorrnopnlem.n . . . . . . . . . 10 (𝜑𝑋 ≠ ∅)
514, 49, 40, 50rnmptn0 41691 . . . . . . . . 9 (𝜑 → ran (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖)))) ≠ ∅)
5214, 51eqnetrd 3080 . . . . . . . 8 (𝜑𝐻 ≠ ∅)
53 rpssre 12382 . . . . . . . . . 10 + ⊆ ℝ
5453a1i 11 . . . . . . . . 9 (𝜑 → ℝ+ ⊆ ℝ)
5543, 54sstrd 3961 . . . . . . . 8 (𝜑𝐻 ⊆ ℝ)
56 fiinfcl 8949 . . . . . . . 8 (( < Or ℝ ∧ (𝐻 ∈ Fin ∧ 𝐻 ≠ ∅ ∧ 𝐻 ⊆ ℝ)) → inf(𝐻, ℝ, < ) ∈ 𝐻)
5745, 48, 52, 55, 56syl13anc 1369 . . . . . . 7 (𝜑 → inf(𝐻, ℝ, < ) ∈ 𝐻)
5843, 57sseldd 3952 . . . . . 6 (𝜑 → inf(𝐻, ℝ, < ) ∈ ℝ+)
5912, 58eqeltrid 2920 . . . . 5 (𝜑𝐸 ∈ ℝ+)
60 rpxr 12384 . . . . 5 (𝐸 ∈ ℝ+𝐸 ∈ ℝ*)
6159, 60syl 17 . . . 4 (𝜑𝐸 ∈ ℝ*)
62 eqid 2824 . . . . 5 (MetOpen‘𝐷) = (MetOpen‘𝐷)
6362blopn 23096 . . . 4 ((𝐷 ∈ (∞Met‘(ℝ ↑m 𝑋)) ∧ 𝐹 ∈ (ℝ ↑m 𝑋) ∧ 𝐸 ∈ ℝ*) → (𝐹(ball‘𝐷)𝐸) ∈ (MetOpen‘𝐷))
643, 11, 61, 63syl3anc 1368 . . 3 (𝜑 → (𝐹(ball‘𝐷)𝐸) ∈ (MetOpen‘𝐷))
65 ioorrnopnlem.v . . . . 5 𝑉 = (𝐹(ball‘𝐷)𝐸)
6665a1i 11 . . . 4 (𝜑𝑉 = (𝐹(ball‘𝐷)𝐸))
671rrxtopnfi 42771 . . . . 5 (𝜑 → (TopOpen‘(ℝ^‘𝑋)) = (MetOpen‘(𝑓 ∈ (ℝ ↑m 𝑋), 𝑔 ∈ (ℝ ↑m 𝑋) ↦ (√‘Σ𝑘𝑋 (((𝑓𝑘) − (𝑔𝑘))↑2)))))
682eqcomi 2833 . . . . . . 7 (𝑓 ∈ (ℝ ↑m 𝑋), 𝑔 ∈ (ℝ ↑m 𝑋) ↦ (√‘Σ𝑘𝑋 (((𝑓𝑘) − (𝑔𝑘))↑2))) = 𝐷
6968a1i 11 . . . . . 6 (𝜑 → (𝑓 ∈ (ℝ ↑m 𝑋), 𝑔 ∈ (ℝ ↑m 𝑋) ↦ (√‘Σ𝑘𝑋 (((𝑓𝑘) − (𝑔𝑘))↑2))) = 𝐷)
7069fveq2d 6655 . . . . 5 (𝜑 → (MetOpen‘(𝑓 ∈ (ℝ ↑m 𝑋), 𝑔 ∈ (ℝ ↑m 𝑋) ↦ (√‘Σ𝑘𝑋 (((𝑓𝑘) − (𝑔𝑘))↑2)))) = (MetOpen‘𝐷))
7167, 70eqtrd 2859 . . . 4 (𝜑 → (TopOpen‘(ℝ^‘𝑋)) = (MetOpen‘𝐷))
7266, 71eleq12d 2910 . . 3 (𝜑 → (𝑉 ∈ (TopOpen‘(ℝ^‘𝑋)) ↔ (𝐹(ball‘𝐷)𝐸) ∈ (MetOpen‘𝐷)))
7364, 72mpbird 260 . 2 (𝜑𝑉 ∈ (TopOpen‘(ℝ^‘𝑋)))
74 xmetpsmet 22944 . . . . . 6 (𝐷 ∈ (∞Met‘(ℝ ↑m 𝑋)) → 𝐷 ∈ (PsMet‘(ℝ ↑m 𝑋)))
753, 74syl 17 . . . . 5 (𝜑𝐷 ∈ (PsMet‘(ℝ ↑m 𝑋)))
76 blcntrps 23008 . . . . 5 ((𝐷 ∈ (PsMet‘(ℝ ↑m 𝑋)) ∧ 𝐹 ∈ (ℝ ↑m 𝑋) ∧ 𝐸 ∈ ℝ+) → 𝐹 ∈ (𝐹(ball‘𝐷)𝐸))
7775, 11, 59, 76syl3anc 1368 . . . 4 (𝜑𝐹 ∈ (𝐹(ball‘𝐷)𝐸))
7866eqcomd 2830 . . . 4 (𝜑 → (𝐹(ball‘𝐷)𝐸) = 𝑉)
7977, 78eleqtrd 2918 . . 3 (𝜑𝐹𝑉)
80 nfv 1916 . . . . 5 𝑔𝜑
81 elmapfn 8412 . . . . . . . 8 (𝑔 ∈ (ℝ ↑m 𝑋) → 𝑔 Fn 𝑋)
82813ad2ant2 1131 . . . . . . 7 ((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) → 𝑔 Fn 𝑋)
83253ad2antl1 1182 . . . . . . . . 9 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝐴𝑖) ∈ ℝ*)
84263ad2antl1 1182 . . . . . . . . 9 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝐵𝑖) ∈ ℝ*)
85 simpl2 1189 . . . . . . . . . 10 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → 𝑔 ∈ (ℝ ↑m 𝑋))
86 simpr 488 . . . . . . . . . 10 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → 𝑖𝑋)
87 elmapi 8411 . . . . . . . . . . . 12 (𝑔 ∈ (ℝ ↑m 𝑋) → 𝑔:𝑋⟶ℝ)
8887adantr 484 . . . . . . . . . . 11 ((𝑔 ∈ (ℝ ↑m 𝑋) ∧ 𝑖𝑋) → 𝑔:𝑋⟶ℝ)
89 simpr 488 . . . . . . . . . . 11 ((𝑔 ∈ (ℝ ↑m 𝑋) ∧ 𝑖𝑋) → 𝑖𝑋)
9088, 89ffvelrnd 6833 . . . . . . . . . 10 ((𝑔 ∈ (ℝ ↑m 𝑋) ∧ 𝑖𝑋) → (𝑔𝑖) ∈ ℝ)
9185, 86, 90syl2anc 587 . . . . . . . . 9 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝑔𝑖) ∈ ℝ)
92243ad2antl1 1182 . . . . . . . . . 10 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝐴𝑖) ∈ ℝ)
9353, 59sseldi 3949 . . . . . . . . . . . . 13 (𝜑𝐸 ∈ ℝ)
9493adantr 484 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → 𝐸 ∈ ℝ)
9521, 94resubcld 11053 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → ((𝐹𝑖) − 𝐸) ∈ ℝ)
96953ad2antl1 1182 . . . . . . . . . 10 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → ((𝐹𝑖) − 𝐸) ∈ ℝ)
9753, 38sseldi 3949 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ∈ ℝ)
9812a1i 11 . . . . . . . . . . . . . . . 16 (𝜑𝐸 = inf(𝐻, ℝ, < ))
99 infxrrefi 41858 . . . . . . . . . . . . . . . . . 18 ((𝐻 ⊆ ℝ ∧ 𝐻 ∈ Fin ∧ 𝐻 ≠ ∅) → inf(𝐻, ℝ*, < ) = inf(𝐻, ℝ, < ))
10055, 48, 52, 99syl3anc 1368 . . . . . . . . . . . . . . . . 17 (𝜑 → inf(𝐻, ℝ*, < ) = inf(𝐻, ℝ, < ))
101100eqcomd 2830 . . . . . . . . . . . . . . . 16 (𝜑 → inf(𝐻, ℝ, < ) = inf(𝐻, ℝ*, < ))
10298, 101eqtrd 2859 . . . . . . . . . . . . . . 15 (𝜑𝐸 = inf(𝐻, ℝ*, < ))
103102adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋) → 𝐸 = inf(𝐻, ℝ*, < ))
104 ressxr 10670 . . . . . . . . . . . . . . . . . 18 ℝ ⊆ ℝ*
105104a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → ℝ ⊆ ℝ*)
10655, 105sstrd 3961 . . . . . . . . . . . . . . . 16 (𝜑𝐻 ⊆ ℝ*)
107106adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑋) → 𝐻 ⊆ ℝ*)
10840elrnmpt1 5811 . . . . . . . . . . . . . . . . 17 ((𝑖𝑋 ∧ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ∈ V) → if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ∈ ran (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖)))))
10918, 49, 108syl2anc 587 . . . . . . . . . . . . . . . 16 ((𝜑𝑖𝑋) → if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ∈ ran (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖)))))
110109, 13eleqtrrdi 2927 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑋) → if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ∈ 𝐻)
111 infxrlb 12713 . . . . . . . . . . . . . . 15 ((𝐻 ⊆ ℝ* ∧ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ∈ 𝐻) → inf(𝐻, ℝ*, < ) ≤ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))))
112107, 110, 111syl2anc 587 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋) → inf(𝐻, ℝ*, < ) ≤ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))))
113103, 112eqbrtrd 5069 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → 𝐸 ≤ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))))
114 min2 12569 . . . . . . . . . . . . . 14 ((((𝐵𝑖) − (𝐹𝑖)) ∈ ℝ ∧ ((𝐹𝑖) − (𝐴𝑖)) ∈ ℝ) → if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ≤ ((𝐹𝑖) − (𝐴𝑖)))
11522, 32, 114syl2anc 587 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ≤ ((𝐹𝑖) − (𝐴𝑖)))
11694, 97, 32, 113, 115letrd 10782 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → 𝐸 ≤ ((𝐹𝑖) − (𝐴𝑖)))
11794, 21, 24, 116lesubd 11229 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → (𝐴𝑖) ≤ ((𝐹𝑖) − 𝐸))
1181173ad2antl1 1182 . . . . . . . . . 10 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝐴𝑖) ≤ ((𝐹𝑖) − 𝐸))
11921adantlr 714 . . . . . . . . . . . . . 14 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → (𝐹𝑖) ∈ ℝ)
12090adantll 713 . . . . . . . . . . . . . 14 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → (𝑔𝑖) ∈ ℝ)
121119, 120resubcld 11053 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → ((𝐹𝑖) − (𝑔𝑖)) ∈ ℝ)
1221213adantl3 1165 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → ((𝐹𝑖) − (𝑔𝑖)) ∈ ℝ)
1231, 2rrndsmet 42786 . . . . . . . . . . . . . . 15 (𝜑𝐷 ∈ (Met‘(ℝ ↑m 𝑋)))
124123ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → 𝐷 ∈ (Met‘(ℝ ↑m 𝑋)))
12511ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → 𝐹 ∈ (ℝ ↑m 𝑋))
126 simplr 768 . . . . . . . . . . . . . 14 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → 𝑔 ∈ (ℝ ↑m 𝑋))
127 metcl 22928 . . . . . . . . . . . . . 14 ((𝐷 ∈ (Met‘(ℝ ↑m 𝑋)) ∧ 𝐹 ∈ (ℝ ↑m 𝑋) ∧ 𝑔 ∈ (ℝ ↑m 𝑋)) → (𝐹𝐷𝑔) ∈ ℝ)
128124, 125, 126, 127syl3anc 1368 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → (𝐹𝐷𝑔) ∈ ℝ)
1291283adantl3 1165 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝐹𝐷𝑔) ∈ ℝ)
13094adantlr 714 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → 𝐸 ∈ ℝ)
1311303adantl3 1165 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → 𝐸 ∈ ℝ)
132121recnd 10654 . . . . . . . . . . . . . . 15 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → ((𝐹𝑖) − (𝑔𝑖)) ∈ ℂ)
133132abscld 14785 . . . . . . . . . . . . . 14 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → (abs‘((𝐹𝑖) − (𝑔𝑖))) ∈ ℝ)
134121leabsd 14763 . . . . . . . . . . . . . 14 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → ((𝐹𝑖) − (𝑔𝑖)) ≤ (abs‘((𝐹𝑖) − (𝑔𝑖))))
1351ad2antrr 725 . . . . . . . . . . . . . . . 16 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → 𝑋 ∈ Fin)
136 ixpf 8467 . . . . . . . . . . . . . . . . . . 19 (𝐹X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)) → 𝐹:𝑋 𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))
13710, 136syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹:𝑋 𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))
1388ralrimiva 3176 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)) ⊆ ℝ)
139 iunss 4950 . . . . . . . . . . . . . . . . . . 19 ( 𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)) ⊆ ℝ ↔ ∀𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)) ⊆ ℝ)
140138, 139sylibr 237 . . . . . . . . . . . . . . . . . 18 (𝜑 𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)) ⊆ ℝ)
141137, 140fssd 6509 . . . . . . . . . . . . . . . . 17 (𝜑𝐹:𝑋⟶ℝ)
142141ad2antrr 725 . . . . . . . . . . . . . . . 16 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → 𝐹:𝑋⟶ℝ)
143126, 87syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → 𝑔:𝑋⟶ℝ)
144 simpr 488 . . . . . . . . . . . . . . . 16 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → 𝑖𝑋)
145 eqid 2824 . . . . . . . . . . . . . . . 16 (dist‘(ℝ^‘𝑋)) = (dist‘(ℝ^‘𝑋))
146135, 142, 143, 144, 145rrnprjdstle 42785 . . . . . . . . . . . . . . 15 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → (abs‘((𝐹𝑖) − (𝑔𝑖))) ≤ (𝐹(dist‘(ℝ^‘𝑋))𝑔))
147 eqid 2824 . . . . . . . . . . . . . . . . . . . 20 (ℝ^‘𝑋) = (ℝ^‘𝑋)
148 eqid 2824 . . . . . . . . . . . . . . . . . . . 20 (ℝ ↑m 𝑋) = (ℝ ↑m 𝑋)
149147, 148rrxdsfi 24004 . . . . . . . . . . . . . . . . . . 19 (𝑋 ∈ Fin → (dist‘(ℝ^‘𝑋)) = (𝑓 ∈ (ℝ ↑m 𝑋), 𝑔 ∈ (ℝ ↑m 𝑋) ↦ (√‘Σ𝑘𝑋 (((𝑓𝑘) − (𝑔𝑘))↑2))))
1501, 149syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (dist‘(ℝ^‘𝑋)) = (𝑓 ∈ (ℝ ↑m 𝑋), 𝑔 ∈ (ℝ ↑m 𝑋) ↦ (√‘Σ𝑘𝑋 (((𝑓𝑘) − (𝑔𝑘))↑2))))
151150, 69eqtrd 2859 . . . . . . . . . . . . . . . . 17 (𝜑 → (dist‘(ℝ^‘𝑋)) = 𝐷)
152151oveqd 7155 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹(dist‘(ℝ^‘𝑋))𝑔) = (𝐹𝐷𝑔))
153152ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → (𝐹(dist‘(ℝ^‘𝑋))𝑔) = (𝐹𝐷𝑔))
154146, 153breqtrd 5073 . . . . . . . . . . . . . 14 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → (abs‘((𝐹𝑖) − (𝑔𝑖))) ≤ (𝐹𝐷𝑔))
155121, 133, 128, 134, 154letrd 10782 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → ((𝐹𝑖) − (𝑔𝑖)) ≤ (𝐹𝐷𝑔))
1561553adantl3 1165 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → ((𝐹𝑖) − (𝑔𝑖)) ≤ (𝐹𝐷𝑔))
157 simpl3 1190 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝐹𝐷𝑔) < 𝐸)
158122, 129, 131, 156, 157lelttrd 10783 . . . . . . . . . . 11 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → ((𝐹𝑖) − (𝑔𝑖)) < 𝐸)
159 ltsub23 11105 . . . . . . . . . . . . 13 (((𝐹𝑖) ∈ ℝ ∧ (𝑔𝑖) ∈ ℝ ∧ 𝐸 ∈ ℝ) → (((𝐹𝑖) − (𝑔𝑖)) < 𝐸 ↔ ((𝐹𝑖) − 𝐸) < (𝑔𝑖)))
160119, 120, 130, 159syl3anc 1368 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → (((𝐹𝑖) − (𝑔𝑖)) < 𝐸 ↔ ((𝐹𝑖) − 𝐸) < (𝑔𝑖)))
1611603adantl3 1165 . . . . . . . . . . 11 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (((𝐹𝑖) − (𝑔𝑖)) < 𝐸 ↔ ((𝐹𝑖) − 𝐸) < (𝑔𝑖)))
162158, 161mpbid 235 . . . . . . . . . 10 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → ((𝐹𝑖) − 𝐸) < (𝑔𝑖))
16392, 96, 91, 118, 162lelttrd 10783 . . . . . . . . 9 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝐴𝑖) < (𝑔𝑖))
16421, 94readdcld 10655 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → ((𝐹𝑖) + 𝐸) ∈ ℝ)
1651643ad2antl1 1182 . . . . . . . . . 10 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → ((𝐹𝑖) + 𝐸) ∈ ℝ)
166163ad2antl1 1182 . . . . . . . . . 10 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝐵𝑖) ∈ ℝ)
167120, 119resubcld 11053 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → ((𝑔𝑖) − (𝐹𝑖)) ∈ ℝ)
1681673adantl3 1165 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → ((𝑔𝑖) − (𝐹𝑖)) ∈ ℝ)
169167leabsd 14763 . . . . . . . . . . . . . . 15 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → ((𝑔𝑖) − (𝐹𝑖)) ≤ (abs‘((𝑔𝑖) − (𝐹𝑖))))
170120recnd 10654 . . . . . . . . . . . . . . . 16 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → (𝑔𝑖) ∈ ℂ)
171119recnd 10654 . . . . . . . . . . . . . . . 16 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → (𝐹𝑖) ∈ ℂ)
172170, 171abssubd 14802 . . . . . . . . . . . . . . 15 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → (abs‘((𝑔𝑖) − (𝐹𝑖))) = (abs‘((𝐹𝑖) − (𝑔𝑖))))
173169, 172breqtrd 5073 . . . . . . . . . . . . . 14 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → ((𝑔𝑖) − (𝐹𝑖)) ≤ (abs‘((𝐹𝑖) − (𝑔𝑖))))
174167, 133, 128, 173, 154letrd 10782 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖𝑋) → ((𝑔𝑖) − (𝐹𝑖)) ≤ (𝐹𝐷𝑔))
1751743adantl3 1165 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → ((𝑔𝑖) − (𝐹𝑖)) ≤ (𝐹𝐷𝑔))
176168, 129, 131, 175, 157lelttrd 10783 . . . . . . . . . . 11 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → ((𝑔𝑖) − (𝐹𝑖)) < 𝐸)
1771193adantl3 1165 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝐹𝑖) ∈ ℝ)
17891, 177, 131ltsubadd2d 11223 . . . . . . . . . . 11 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (((𝑔𝑖) − (𝐹𝑖)) < 𝐸 ↔ (𝑔𝑖) < ((𝐹𝑖) + 𝐸)))
179176, 178mpbid 235 . . . . . . . . . 10 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝑔𝑖) < ((𝐹𝑖) + 𝐸))
180 min1 12568 . . . . . . . . . . . . . 14 ((((𝐵𝑖) − (𝐹𝑖)) ∈ ℝ ∧ ((𝐹𝑖) − (𝐴𝑖)) ∈ ℝ) → if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ≤ ((𝐵𝑖) − (𝐹𝑖)))
18122, 32, 180syl2anc 587 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ≤ ((𝐵𝑖) − (𝐹𝑖)))
18294, 97, 22, 113, 181letrd 10782 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → 𝐸 ≤ ((𝐵𝑖) − (𝐹𝑖)))
18321, 94, 16leaddsub2d 11227 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → (((𝐹𝑖) + 𝐸) ≤ (𝐵𝑖) ↔ 𝐸 ≤ ((𝐵𝑖) − (𝐹𝑖))))
184182, 183mpbird 260 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → ((𝐹𝑖) + 𝐸) ≤ (𝐵𝑖))
1851843ad2antl1 1182 . . . . . . . . . 10 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → ((𝐹𝑖) + 𝐸) ≤ (𝐵𝑖))
18691, 165, 166, 179, 185ltletrd 10785 . . . . . . . . 9 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝑔𝑖) < (𝐵𝑖))
18783, 84, 91, 163, 186eliood 41977 . . . . . . . 8 (((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝑔𝑖) ∈ ((𝐴𝑖)(,)(𝐵𝑖)))
188187ralrimiva 3176 . . . . . . 7 ((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) → ∀𝑖𝑋 (𝑔𝑖) ∈ ((𝐴𝑖)(,)(𝐵𝑖)))
18982, 188jca 515 . . . . . 6 ((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) → (𝑔 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑔𝑖) ∈ ((𝐴𝑖)(,)(𝐵𝑖))))
190 vex 3482 . . . . . . 7 𝑔 ∈ V
191190elixp 8451 . . . . . 6 (𝑔X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)) ↔ (𝑔 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑔𝑖) ∈ ((𝐴𝑖)(,)(𝐵𝑖))))
192189, 191sylibr 237 . . . . 5 ((𝜑𝑔 ∈ (ℝ ↑m 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) → 𝑔X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))
19380, 75, 11, 61, 192ballss3 41567 . . . 4 (𝜑 → (𝐹(ball‘𝐷)𝐸) ⊆ X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))
19466, 193eqsstrd 3989 . . 3 (𝜑𝑉X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))
19579, 194jca 515 . 2 (𝜑 → (𝐹𝑉𝑉X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖))))
196 eleq2 2904 . . . 4 (𝑣 = 𝑉 → (𝐹𝑣𝐹𝑉))
197 sseq1 3976 . . . 4 (𝑣 = 𝑉 → (𝑣X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)) ↔ 𝑉X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖))))
198196, 197anbi12d 633 . . 3 (𝑣 = 𝑉 → ((𝐹𝑣𝑣X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖))) ↔ (𝐹𝑉𝑉X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))))
199198rspcev 3608 . 2 ((𝑉 ∈ (TopOpen‘(ℝ^‘𝑋)) ∧ (𝐹𝑉𝑉X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))) → ∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝐹𝑣𝑣X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖))))
20073, 195, 199syl2anc 587 1 (𝜑 → ∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝐹𝑣𝑣X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2115  wne 3013  wral 3132  wrex 3133  Vcvv 3479  wss 3918  c0 4274  ifcif 4448   ciun 4900   class class class wbr 5047  cmpt 5127   Or wor 5454  ran crn 5537   Fn wfn 6331  wf 6332  cfv 6336  (class class class)co 7138  cmpo 7140  m cmap 8389  Xcixp 8444  Fincfn 8492  infcinf 8889  cr 10521  0cc0 10522   + caddc 10525  *cxr 10659   < clt 10660  cle 10661  cmin 10855  2c2 11678  +crp 12375  (,)cioo 12724  cexp 13423  csqrt 14581  abscabs 14582  Σcsu 15031  distcds 16563  TopOpenctopn 16684  PsMetcpsmet 20515  ∞Metcxmet 20516  Metcmet 20517  ballcbl 20518  MetOpencmopn 20521  ℝ^crrx 23976
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5171  ax-sep 5184  ax-nul 5191  ax-pow 5247  ax-pr 5311  ax-un 7444  ax-inf2 9088  ax-cnex 10578  ax-resscn 10579  ax-1cn 10580  ax-icn 10581  ax-addcl 10582  ax-addrcl 10583  ax-mulcl 10584  ax-mulrcl 10585  ax-mulcom 10586  ax-addass 10587  ax-mulass 10588  ax-distr 10589  ax-i2m1 10590  ax-1ne0 10591  ax-1rid 10592  ax-rnegex 10593  ax-rrecex 10594  ax-cnre 10595  ax-pre-lttri 10596  ax-pre-lttrn 10597  ax-pre-ltadd 10598  ax-pre-mulgt0 10599  ax-pre-sup 10600  ax-addf 10601  ax-mulf 10602
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3014  df-nel 3118  df-ral 3137  df-rex 3138  df-reu 3139  df-rmo 3140  df-rab 3141  df-v 3481  df-sbc 3758  df-csb 3866  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-pss 3937  df-nul 4275  df-if 4449  df-pw 4522  df-sn 4549  df-pr 4551  df-tp 4553  df-op 4555  df-uni 4820  df-int 4858  df-iun 4902  df-br 5048  df-opab 5110  df-mpt 5128  df-tr 5154  df-id 5441  df-eprel 5446  df-po 5455  df-so 5456  df-fr 5495  df-se 5496  df-we 5497  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-pred 6129  df-ord 6175  df-on 6176  df-lim 6177  df-suc 6178  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-isom 6345  df-riota 7096  df-ov 7141  df-oprab 7142  df-mpo 7143  df-of 7392  df-om 7564  df-1st 7672  df-2nd 7673  df-supp 7814  df-tpos 7875  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-1o 8085  df-oadd 8089  df-er 8272  df-map 8391  df-ixp 8445  df-en 8493  df-dom 8494  df-sdom 8495  df-fin 8496  df-fsupp 8818  df-sup 8890  df-inf 8891  df-oi 8958  df-card 9352  df-pnf 10662  df-mnf 10663  df-xr 10664  df-ltxr 10665  df-le 10666  df-sub 10857  df-neg 10858  df-div 11283  df-nn 11624  df-2 11686  df-3 11687  df-4 11688  df-5 11689  df-6 11690  df-7 11691  df-8 11692  df-9 11693  df-n0 11884  df-z 11968  df-dec 12085  df-uz 12230  df-q 12335  df-rp 12376  df-xneg 12493  df-xadd 12494  df-xmul 12495  df-ioo 12728  df-ico 12730  df-fz 12884  df-fzo 13027  df-seq 13363  df-exp 13424  df-hash 13685  df-cj 14447  df-re 14448  df-im 14449  df-sqrt 14583  df-abs 14584  df-clim 14834  df-sum 15032  df-struct 16474  df-ndx 16475  df-slot 16476  df-base 16478  df-sets 16479  df-ress 16480  df-plusg 16567  df-mulr 16568  df-starv 16569  df-sca 16570  df-vsca 16571  df-ip 16572  df-tset 16573  df-ple 16574  df-ds 16576  df-unif 16577  df-hom 16578  df-cco 16579  df-rest 16685  df-topn 16686  df-0g 16704  df-gsum 16705  df-topgen 16706  df-prds 16710  df-pws 16712  df-mgm 17841  df-sgrp 17890  df-mnd 17901  df-mhm 17945  df-grp 18095  df-minusg 18096  df-sbg 18097  df-subg 18265  df-ghm 18345  df-cntz 18436  df-cmn 18897  df-abl 18898  df-mgp 19229  df-ur 19241  df-ring 19288  df-cring 19289  df-oppr 19362  df-dvdsr 19380  df-unit 19381  df-invr 19411  df-dvr 19422  df-rnghom 19456  df-drng 19490  df-field 19491  df-subrg 19519  df-staf 19602  df-srng 19603  df-lmod 19622  df-lss 19690  df-sra 19930  df-rgmod 19931  df-psmet 20523  df-xmet 20524  df-met 20525  df-bl 20526  df-mopn 20527  df-cnfld 20532  df-refld 20735  df-dsmm 20862  df-frlm 20877  df-top 21488  df-topon 21505  df-bases 21540  df-nm 23178  df-tng 23180  df-tcph 23763  df-rrx 23978
This theorem is referenced by:  ioorrnopn  42789
  Copyright terms: Public domain W3C validator