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 41041
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 𝐷 = (𝑓 ∈ (ℝ ↑𝑚 𝑋), 𝑔 ∈ (ℝ ↑𝑚 𝑋) ↦ (√‘Σ𝑘𝑋 (((𝑓𝑘) − (𝑔𝑘))↑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 𝐷 = (𝑓 ∈ (ℝ ↑𝑚 𝑋), 𝑔 ∈ (ℝ ↑𝑚 𝑋) ↦ (√‘Σ𝑘𝑋 (((𝑓𝑘) − (𝑔𝑘))↑2)))
31, 2rrndsxmet 41040 . . . 4 (𝜑𝐷 ∈ (∞Met‘(ℝ ↑𝑚 𝑋)))
4 nfv 1995 . . . . . 6 𝑖𝜑
5 reex 10229 . . . . . . 7 ℝ ∈ V
65a1i 11 . . . . . 6 (𝜑 → ℝ ∈ V)
7 ioossre 12440 . . . . . . 7 ((𝐴𝑖)(,)(𝐵𝑖)) ⊆ ℝ
87a1i 11 . . . . . 6 ((𝜑𝑖𝑋) → ((𝐴𝑖)(,)(𝐵𝑖)) ⊆ ℝ)
94, 6, 8ixpssmapc 39764 . . . . 5 (𝜑X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)) ⊆ (ℝ ↑𝑚 𝑋))
10 ioorrnopnlem.f . . . . 5 (𝜑𝐹X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))
119, 10sseldd 3753 . . . 4 (𝜑𝐹 ∈ (ℝ ↑𝑚 𝑋))
12 ioorrnopnlem.e . . . . . 6 𝐸 = inf(𝐻, ℝ, < )
13 ioorrnopnlem.h . . . . . . . . 9 𝐻 = ran (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))))
1413a1i 11 . . . . . . . 8 (𝜑𝐻 = ran (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖)))))
15 ioorrnopnlem.b . . . . . . . . . . . . . 14 (𝜑𝐵:𝑋⟶ℝ)
1615ffvelrnda 6502 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → (𝐵𝑖) ∈ ℝ)
1710adantr 466 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑋) → 𝐹X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))
18 simpr 471 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑋) → 𝑖𝑋)
19 fvixp2 39908 . . . . . . . . . . . . . . 15 ((𝐹X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)) ∧ 𝑖𝑋) → (𝐹𝑖) ∈ ((𝐴𝑖)(,)(𝐵𝑖)))
2017, 18, 19syl2anc 573 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋) → (𝐹𝑖) ∈ ((𝐴𝑖)(,)(𝐵𝑖)))
217, 20sseldi 3750 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → (𝐹𝑖) ∈ ℝ)
2216, 21resubcld 10660 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → ((𝐵𝑖) − (𝐹𝑖)) ∈ ℝ)
23 ioorrnopnlem.a . . . . . . . . . . . . . . . 16 (𝜑𝐴:𝑋⟶ℝ)
2423ffvelrnda 6502 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑋) → (𝐴𝑖) ∈ ℝ)
2524rexrd 10291 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋) → (𝐴𝑖) ∈ ℝ*)
2616rexrd 10291 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋) → (𝐵𝑖) ∈ ℝ*)
27 iooltub 40255 . . . . . . . . . . . . . 14 (((𝐴𝑖) ∈ ℝ* ∧ (𝐵𝑖) ∈ ℝ* ∧ (𝐹𝑖) ∈ ((𝐴𝑖)(,)(𝐵𝑖))) → (𝐹𝑖) < (𝐵𝑖))
2825, 26, 20, 27syl3anc 1476 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → (𝐹𝑖) < (𝐵𝑖))
2921, 16posdifd 10816 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → ((𝐹𝑖) < (𝐵𝑖) ↔ 0 < ((𝐵𝑖) − (𝐹𝑖))))
3028, 29mpbid 222 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → 0 < ((𝐵𝑖) − (𝐹𝑖)))
3122, 30elrpd 12072 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → ((𝐵𝑖) − (𝐹𝑖)) ∈ ℝ+)
3221, 24resubcld 10660 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → ((𝐹𝑖) − (𝐴𝑖)) ∈ ℝ)
33 ioogtlb 40238 . . . . . . . . . . . . . 14 (((𝐴𝑖) ∈ ℝ* ∧ (𝐵𝑖) ∈ ℝ* ∧ (𝐹𝑖) ∈ ((𝐴𝑖)(,)(𝐵𝑖))) → (𝐴𝑖) < (𝐹𝑖))
3425, 26, 20, 33syl3anc 1476 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → (𝐴𝑖) < (𝐹𝑖))
3524, 21posdifd 10816 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → ((𝐴𝑖) < (𝐹𝑖) ↔ 0 < ((𝐹𝑖) − (𝐴𝑖))))
3634, 35mpbid 222 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → 0 < ((𝐹𝑖) − (𝐴𝑖)))
3732, 36elrpd 12072 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → ((𝐹𝑖) − (𝐴𝑖)) ∈ ℝ+)
3831, 37ifcld 4270 . . . . . . . . . 10 ((𝜑𝑖𝑋) → if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ∈ ℝ+)
3938ralrimiva 3115 . . . . . . . . 9 (𝜑 → ∀𝑖𝑋 if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ∈ ℝ+)
40 eqid 2771 . . . . . . . . . 10 (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖)))) = (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))))
4140rnmptss 6534 . . . . . . . . 9 (∀𝑖𝑋 if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ∈ ℝ+ → ran (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖)))) ⊆ ℝ+)
4239, 41syl 17 . . . . . . . 8 (𝜑 → ran (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖)))) ⊆ ℝ+)
4314, 42eqsstrd 3788 . . . . . . 7 (𝜑𝐻 ⊆ ℝ+)
44 ltso 10320 . . . . . . . . 9 < Or ℝ
4544a1i 11 . . . . . . . 8 (𝜑 → < Or ℝ)
4640rnmptfi 39871 . . . . . . . . . 10 (𝑋 ∈ Fin → ran (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖)))) ∈ Fin)
471, 46syl 17 . . . . . . . . 9 (𝜑 → ran (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖)))) ∈ Fin)
4813, 47syl5eqel 2854 . . . . . . . 8 (𝜑𝐻 ∈ Fin)
4938elexd 3366 . . . . . . . . . 10 ((𝜑𝑖𝑋) → if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ∈ V)
50 ioorrnopnlem.n . . . . . . . . . 10 (𝜑𝑋 ≠ ∅)
514, 49, 40, 50rnmptn0 39931 . . . . . . . . 9 (𝜑 → ran (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖)))) ≠ ∅)
5214, 51eqnetrd 3010 . . . . . . . 8 (𝜑𝐻 ≠ ∅)
53 rpssre 12046 . . . . . . . . . 10 + ⊆ ℝ
5453a1i 11 . . . . . . . . 9 (𝜑 → ℝ+ ⊆ ℝ)
5543, 54sstrd 3762 . . . . . . . 8 (𝜑𝐻 ⊆ ℝ)
56 fiinfcl 8563 . . . . . . . 8 (( < Or ℝ ∧ (𝐻 ∈ Fin ∧ 𝐻 ≠ ∅ ∧ 𝐻 ⊆ ℝ)) → inf(𝐻, ℝ, < ) ∈ 𝐻)
5745, 48, 52, 55, 56syl13anc 1478 . . . . . . 7 (𝜑 → inf(𝐻, ℝ, < ) ∈ 𝐻)
5843, 57sseldd 3753 . . . . . 6 (𝜑 → inf(𝐻, ℝ, < ) ∈ ℝ+)
5912, 58syl5eqel 2854 . . . . 5 (𝜑𝐸 ∈ ℝ+)
60 rpxr 12043 . . . . 5 (𝐸 ∈ ℝ+𝐸 ∈ ℝ*)
6159, 60syl 17 . . . 4 (𝜑𝐸 ∈ ℝ*)
62 eqid 2771 . . . . 5 (MetOpen‘𝐷) = (MetOpen‘𝐷)
6362blopn 22525 . . . 4 ((𝐷 ∈ (∞Met‘(ℝ ↑𝑚 𝑋)) ∧ 𝐹 ∈ (ℝ ↑𝑚 𝑋) ∧ 𝐸 ∈ ℝ*) → (𝐹(ball‘𝐷)𝐸) ∈ (MetOpen‘𝐷))
643, 11, 61, 63syl3anc 1476 . . 3 (𝜑 → (𝐹(ball‘𝐷)𝐸) ∈ (MetOpen‘𝐷))
65 ioorrnopnlem.v . . . . 5 𝑉 = (𝐹(ball‘𝐷)𝐸)
6665a1i 11 . . . 4 (𝜑𝑉 = (𝐹(ball‘𝐷)𝐸))
671rrxtopnfi 41023 . . . . 5 (𝜑 → (TopOpen‘(ℝ^‘𝑋)) = (MetOpen‘(𝑓 ∈ (ℝ ↑𝑚 𝑋), 𝑔 ∈ (ℝ ↑𝑚 𝑋) ↦ (√‘Σ𝑘𝑋 (((𝑓𝑘) − (𝑔𝑘))↑2)))))
682eqcomi 2780 . . . . . . 7 (𝑓 ∈ (ℝ ↑𝑚 𝑋), 𝑔 ∈ (ℝ ↑𝑚 𝑋) ↦ (√‘Σ𝑘𝑋 (((𝑓𝑘) − (𝑔𝑘))↑2))) = 𝐷
6968a1i 11 . . . . . 6 (𝜑 → (𝑓 ∈ (ℝ ↑𝑚 𝑋), 𝑔 ∈ (ℝ ↑𝑚 𝑋) ↦ (√‘Σ𝑘𝑋 (((𝑓𝑘) − (𝑔𝑘))↑2))) = 𝐷)
7069fveq2d 6336 . . . . 5 (𝜑 → (MetOpen‘(𝑓 ∈ (ℝ ↑𝑚 𝑋), 𝑔 ∈ (ℝ ↑𝑚 𝑋) ↦ (√‘Σ𝑘𝑋 (((𝑓𝑘) − (𝑔𝑘))↑2)))) = (MetOpen‘𝐷))
7167, 70eqtrd 2805 . . . 4 (𝜑 → (TopOpen‘(ℝ^‘𝑋)) = (MetOpen‘𝐷))
7266, 71eleq12d 2844 . . 3 (𝜑 → (𝑉 ∈ (TopOpen‘(ℝ^‘𝑋)) ↔ (𝐹(ball‘𝐷)𝐸) ∈ (MetOpen‘𝐷)))
7364, 72mpbird 247 . 2 (𝜑𝑉 ∈ (TopOpen‘(ℝ^‘𝑋)))
74 xmetpsmet 22373 . . . . . 6 (𝐷 ∈ (∞Met‘(ℝ ↑𝑚 𝑋)) → 𝐷 ∈ (PsMet‘(ℝ ↑𝑚 𝑋)))
753, 74syl 17 . . . . 5 (𝜑𝐷 ∈ (PsMet‘(ℝ ↑𝑚 𝑋)))
76 blcntrps 22437 . . . . 5 ((𝐷 ∈ (PsMet‘(ℝ ↑𝑚 𝑋)) ∧ 𝐹 ∈ (ℝ ↑𝑚 𝑋) ∧ 𝐸 ∈ ℝ+) → 𝐹 ∈ (𝐹(ball‘𝐷)𝐸))
7775, 11, 59, 76syl3anc 1476 . . . 4 (𝜑𝐹 ∈ (𝐹(ball‘𝐷)𝐸))
7866eqcomd 2777 . . . 4 (𝜑 → (𝐹(ball‘𝐷)𝐸) = 𝑉)
7977, 78eleqtrd 2852 . . 3 (𝜑𝐹𝑉)
80 nfv 1995 . . . . 5 𝑔𝜑
81 elmapfn 8032 . . . . . . . 8 (𝑔 ∈ (ℝ ↑𝑚 𝑋) → 𝑔 Fn 𝑋)
82813ad2ant2 1128 . . . . . . 7 ((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) → 𝑔 Fn 𝑋)
83253ad2antl1 1200 . . . . . . . . 9 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝐴𝑖) ∈ ℝ*)
84263ad2antl1 1200 . . . . . . . . 9 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝐵𝑖) ∈ ℝ*)
85 simpl2 1229 . . . . . . . . . 10 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → 𝑔 ∈ (ℝ ↑𝑚 𝑋))
86 simpr 471 . . . . . . . . . 10 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → 𝑖𝑋)
87 elmapi 8031 . . . . . . . . . . . 12 (𝑔 ∈ (ℝ ↑𝑚 𝑋) → 𝑔:𝑋⟶ℝ)
8887adantr 466 . . . . . . . . . . 11 ((𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ 𝑖𝑋) → 𝑔:𝑋⟶ℝ)
89 simpr 471 . . . . . . . . . . 11 ((𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ 𝑖𝑋) → 𝑖𝑋)
9088, 89ffvelrnd 6503 . . . . . . . . . 10 ((𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ 𝑖𝑋) → (𝑔𝑖) ∈ ℝ)
9185, 86, 90syl2anc 573 . . . . . . . . 9 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝑔𝑖) ∈ ℝ)
92243ad2antl1 1200 . . . . . . . . . 10 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝐴𝑖) ∈ ℝ)
9353, 59sseldi 3750 . . . . . . . . . . . . 13 (𝜑𝐸 ∈ ℝ)
9493adantr 466 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → 𝐸 ∈ ℝ)
9521, 94resubcld 10660 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → ((𝐹𝑖) − 𝐸) ∈ ℝ)
96953ad2antl1 1200 . . . . . . . . . 10 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → ((𝐹𝑖) − 𝐸) ∈ ℝ)
9753, 38sseldi 3750 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ∈ ℝ)
9812a1i 11 . . . . . . . . . . . . . . . 16 (𝜑𝐸 = inf(𝐻, ℝ, < ))
99 infxrrefi 40117 . . . . . . . . . . . . . . . . . 18 ((𝐻 ⊆ ℝ ∧ 𝐻 ∈ Fin ∧ 𝐻 ≠ ∅) → inf(𝐻, ℝ*, < ) = inf(𝐻, ℝ, < ))
10055, 48, 52, 99syl3anc 1476 . . . . . . . . . . . . . . . . 17 (𝜑 → inf(𝐻, ℝ*, < ) = inf(𝐻, ℝ, < ))
101100eqcomd 2777 . . . . . . . . . . . . . . . 16 (𝜑 → inf(𝐻, ℝ, < ) = inf(𝐻, ℝ*, < ))
10298, 101eqtrd 2805 . . . . . . . . . . . . . . 15 (𝜑𝐸 = inf(𝐻, ℝ*, < ))
103102adantr 466 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋) → 𝐸 = inf(𝐻, ℝ*, < ))
104 ressxr 10285 . . . . . . . . . . . . . . . . . 18 ℝ ⊆ ℝ*
105104a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → ℝ ⊆ ℝ*)
10655, 105sstrd 3762 . . . . . . . . . . . . . . . 16 (𝜑𝐻 ⊆ ℝ*)
107106adantr 466 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑋) → 𝐻 ⊆ ℝ*)
10840elrnmpt1 5512 . . . . . . . . . . . . . . . . 17 ((𝑖𝑋 ∧ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ∈ V) → if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ∈ ran (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖)))))
10918, 49, 108syl2anc 573 . . . . . . . . . . . . . . . 16 ((𝜑𝑖𝑋) → if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ∈ ran (𝑖𝑋 ↦ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖)))))
110109, 13syl6eleqr 2861 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑋) → if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ∈ 𝐻)
111 infxrlb 12369 . . . . . . . . . . . . . . 15 ((𝐻 ⊆ ℝ* ∧ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ∈ 𝐻) → inf(𝐻, ℝ*, < ) ≤ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))))
112107, 110, 111syl2anc 573 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋) → inf(𝐻, ℝ*, < ) ≤ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))))
113103, 112eqbrtrd 4808 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → 𝐸 ≤ if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))))
114 min2 12226 . . . . . . . . . . . . . 14 ((((𝐵𝑖) − (𝐹𝑖)) ∈ ℝ ∧ ((𝐹𝑖) − (𝐴𝑖)) ∈ ℝ) → if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ≤ ((𝐹𝑖) − (𝐴𝑖)))
11522, 32, 114syl2anc 573 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ≤ ((𝐹𝑖) − (𝐴𝑖)))
11694, 97, 32, 113, 115letrd 10396 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → 𝐸 ≤ ((𝐹𝑖) − (𝐴𝑖)))
11794, 21, 24, 116lesubd 10833 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → (𝐴𝑖) ≤ ((𝐹𝑖) − 𝐸))
1181173ad2antl1 1200 . . . . . . . . . 10 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝐴𝑖) ≤ ((𝐹𝑖) − 𝐸))
11921adantlr 694 . . . . . . . . . . . . . 14 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋)) ∧ 𝑖𝑋) → (𝐹𝑖) ∈ ℝ)
12090adantll 693 . . . . . . . . . . . . . 14 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋)) ∧ 𝑖𝑋) → (𝑔𝑖) ∈ ℝ)
121119, 120resubcld 10660 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋)) ∧ 𝑖𝑋) → ((𝐹𝑖) − (𝑔𝑖)) ∈ ℝ)
1221213adantl3 1173 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → ((𝐹𝑖) − (𝑔𝑖)) ∈ ℝ)
1231, 2rrndsmet 41039 . . . . . . . . . . . . . . 15 (𝜑𝐷 ∈ (Met‘(ℝ ↑𝑚 𝑋)))
124123ad2antrr 705 . . . . . . . . . . . . . 14 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋)) ∧ 𝑖𝑋) → 𝐷 ∈ (Met‘(ℝ ↑𝑚 𝑋)))
12511ad2antrr 705 . . . . . . . . . . . . . 14 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋)) ∧ 𝑖𝑋) → 𝐹 ∈ (ℝ ↑𝑚 𝑋))
126 simplr 752 . . . . . . . . . . . . . 14 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋)) ∧ 𝑖𝑋) → 𝑔 ∈ (ℝ ↑𝑚 𝑋))
127 metcl 22357 . . . . . . . . . . . . . 14 ((𝐷 ∈ (Met‘(ℝ ↑𝑚 𝑋)) ∧ 𝐹 ∈ (ℝ ↑𝑚 𝑋) ∧ 𝑔 ∈ (ℝ ↑𝑚 𝑋)) → (𝐹𝐷𝑔) ∈ ℝ)
128124, 125, 126, 127syl3anc 1476 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋)) ∧ 𝑖𝑋) → (𝐹𝐷𝑔) ∈ ℝ)
1291283adantl3 1173 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝐹𝐷𝑔) ∈ ℝ)
13094adantlr 694 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋)) ∧ 𝑖𝑋) → 𝐸 ∈ ℝ)
1311303adantl3 1173 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → 𝐸 ∈ ℝ)
132121recnd 10270 . . . . . . . . . . . . . . 15 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋)) ∧ 𝑖𝑋) → ((𝐹𝑖) − (𝑔𝑖)) ∈ ℂ)
133132abscld 14383 . . . . . . . . . . . . . 14 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋)) ∧ 𝑖𝑋) → (abs‘((𝐹𝑖) − (𝑔𝑖))) ∈ ℝ)
134121leabsd 14361 . . . . . . . . . . . . . 14 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋)) ∧ 𝑖𝑋) → ((𝐹𝑖) − (𝑔𝑖)) ≤ (abs‘((𝐹𝑖) − (𝑔𝑖))))
1351ad2antrr 705 . . . . . . . . . . . . . . . 16 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋)) ∧ 𝑖𝑋) → 𝑋 ∈ Fin)
136 ixpf 8084 . . . . . . . . . . . . . . . . . . 19 (𝐹X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)) → 𝐹:𝑋 𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))
13710, 136syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹:𝑋 𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))
1388ralrimiva 3115 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)) ⊆ ℝ)
139 iunss 4695 . . . . . . . . . . . . . . . . . . 19 ( 𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)) ⊆ ℝ ↔ ∀𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)) ⊆ ℝ)
140138, 139sylibr 224 . . . . . . . . . . . . . . . . . 18 (𝜑 𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)) ⊆ ℝ)
141137, 140fssd 6197 . . . . . . . . . . . . . . . . 17 (𝜑𝐹:𝑋⟶ℝ)
142141ad2antrr 705 . . . . . . . . . . . . . . . 16 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋)) ∧ 𝑖𝑋) → 𝐹:𝑋⟶ℝ)
143126, 87syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋)) ∧ 𝑖𝑋) → 𝑔:𝑋⟶ℝ)
144 simpr 471 . . . . . . . . . . . . . . . 16 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋)) ∧ 𝑖𝑋) → 𝑖𝑋)
145 eqid 2771 . . . . . . . . . . . . . . . 16 (dist‘(ℝ^‘𝑋)) = (dist‘(ℝ^‘𝑋))
146135, 142, 143, 144, 145rrnprjdstle 41038 . . . . . . . . . . . . . . 15 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋)) ∧ 𝑖𝑋) → (abs‘((𝐹𝑖) − (𝑔𝑖))) ≤ (𝐹(dist‘(ℝ^‘𝑋))𝑔))
147 eqid 2771 . . . . . . . . . . . . . . . . . . . 20 (ℝ^‘𝑋) = (ℝ^‘𝑋)
148 eqid 2771 . . . . . . . . . . . . . . . . . . . 20 (ℝ ↑𝑚 𝑋) = (ℝ ↑𝑚 𝑋)
149147, 148rrxdsfi 41022 . . . . . . . . . . . . . . . . . . 19 (𝑋 ∈ Fin → (dist‘(ℝ^‘𝑋)) = (𝑓 ∈ (ℝ ↑𝑚 𝑋), 𝑔 ∈ (ℝ ↑𝑚 𝑋) ↦ (√‘Σ𝑘𝑋 (((𝑓𝑘) − (𝑔𝑘))↑2))))
1501, 149syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (dist‘(ℝ^‘𝑋)) = (𝑓 ∈ (ℝ ↑𝑚 𝑋), 𝑔 ∈ (ℝ ↑𝑚 𝑋) ↦ (√‘Σ𝑘𝑋 (((𝑓𝑘) − (𝑔𝑘))↑2))))
151150, 69eqtrd 2805 . . . . . . . . . . . . . . . . 17 (𝜑 → (dist‘(ℝ^‘𝑋)) = 𝐷)
152151oveqd 6810 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹(dist‘(ℝ^‘𝑋))𝑔) = (𝐹𝐷𝑔))
153152ad2antrr 705 . . . . . . . . . . . . . . 15 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋)) ∧ 𝑖𝑋) → (𝐹(dist‘(ℝ^‘𝑋))𝑔) = (𝐹𝐷𝑔))
154146, 153breqtrd 4812 . . . . . . . . . . . . . 14 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋)) ∧ 𝑖𝑋) → (abs‘((𝐹𝑖) − (𝑔𝑖))) ≤ (𝐹𝐷𝑔))
155121, 133, 128, 134, 154letrd 10396 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋)) ∧ 𝑖𝑋) → ((𝐹𝑖) − (𝑔𝑖)) ≤ (𝐹𝐷𝑔))
1561553adantl3 1173 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → ((𝐹𝑖) − (𝑔𝑖)) ≤ (𝐹𝐷𝑔))
157 simpl3 1231 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝐹𝐷𝑔) < 𝐸)
158122, 129, 131, 156, 157lelttrd 10397 . . . . . . . . . . 11 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → ((𝐹𝑖) − (𝑔𝑖)) < 𝐸)
159 ltsub23 10710 . . . . . . . . . . . . 13 (((𝐹𝑖) ∈ ℝ ∧ (𝑔𝑖) ∈ ℝ ∧ 𝐸 ∈ ℝ) → (((𝐹𝑖) − (𝑔𝑖)) < 𝐸 ↔ ((𝐹𝑖) − 𝐸) < (𝑔𝑖)))
160119, 120, 130, 159syl3anc 1476 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋)) ∧ 𝑖𝑋) → (((𝐹𝑖) − (𝑔𝑖)) < 𝐸 ↔ ((𝐹𝑖) − 𝐸) < (𝑔𝑖)))
1611603adantl3 1173 . . . . . . . . . . 11 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (((𝐹𝑖) − (𝑔𝑖)) < 𝐸 ↔ ((𝐹𝑖) − 𝐸) < (𝑔𝑖)))
162158, 161mpbid 222 . . . . . . . . . 10 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → ((𝐹𝑖) − 𝐸) < (𝑔𝑖))
16392, 96, 91, 118, 162lelttrd 10397 . . . . . . . . 9 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝐴𝑖) < (𝑔𝑖))
16421, 94readdcld 10271 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → ((𝐹𝑖) + 𝐸) ∈ ℝ)
1651643ad2antl1 1200 . . . . . . . . . 10 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → ((𝐹𝑖) + 𝐸) ∈ ℝ)
166163ad2antl1 1200 . . . . . . . . . 10 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝐵𝑖) ∈ ℝ)
167120, 119resubcld 10660 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋)) ∧ 𝑖𝑋) → ((𝑔𝑖) − (𝐹𝑖)) ∈ ℝ)
1681673adantl3 1173 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → ((𝑔𝑖) − (𝐹𝑖)) ∈ ℝ)
169167leabsd 14361 . . . . . . . . . . . . . . 15 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋)) ∧ 𝑖𝑋) → ((𝑔𝑖) − (𝐹𝑖)) ≤ (abs‘((𝑔𝑖) − (𝐹𝑖))))
170120recnd 10270 . . . . . . . . . . . . . . . 16 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋)) ∧ 𝑖𝑋) → (𝑔𝑖) ∈ ℂ)
171119recnd 10270 . . . . . . . . . . . . . . . 16 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋)) ∧ 𝑖𝑋) → (𝐹𝑖) ∈ ℂ)
172170, 171abssubd 14400 . . . . . . . . . . . . . . 15 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋)) ∧ 𝑖𝑋) → (abs‘((𝑔𝑖) − (𝐹𝑖))) = (abs‘((𝐹𝑖) − (𝑔𝑖))))
173169, 172breqtrd 4812 . . . . . . . . . . . . . 14 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋)) ∧ 𝑖𝑋) → ((𝑔𝑖) − (𝐹𝑖)) ≤ (abs‘((𝐹𝑖) − (𝑔𝑖))))
174167, 133, 128, 173, 154letrd 10396 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋)) ∧ 𝑖𝑋) → ((𝑔𝑖) − (𝐹𝑖)) ≤ (𝐹𝐷𝑔))
1751743adantl3 1173 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → ((𝑔𝑖) − (𝐹𝑖)) ≤ (𝐹𝐷𝑔))
176168, 129, 131, 175, 157lelttrd 10397 . . . . . . . . . . 11 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → ((𝑔𝑖) − (𝐹𝑖)) < 𝐸)
1771193adantl3 1173 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝐹𝑖) ∈ ℝ)
17891, 177, 131ltsubadd2d 10827 . . . . . . . . . . 11 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (((𝑔𝑖) − (𝐹𝑖)) < 𝐸 ↔ (𝑔𝑖) < ((𝐹𝑖) + 𝐸)))
179176, 178mpbid 222 . . . . . . . . . 10 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝑔𝑖) < ((𝐹𝑖) + 𝐸))
180 min1 12225 . . . . . . . . . . . . . 14 ((((𝐵𝑖) − (𝐹𝑖)) ∈ ℝ ∧ ((𝐹𝑖) − (𝐴𝑖)) ∈ ℝ) → if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ≤ ((𝐵𝑖) − (𝐹𝑖)))
18122, 32, 180syl2anc 573 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → if(((𝐵𝑖) − (𝐹𝑖)) ≤ ((𝐹𝑖) − (𝐴𝑖)), ((𝐵𝑖) − (𝐹𝑖)), ((𝐹𝑖) − (𝐴𝑖))) ≤ ((𝐵𝑖) − (𝐹𝑖)))
18294, 97, 22, 113, 181letrd 10396 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → 𝐸 ≤ ((𝐵𝑖) − (𝐹𝑖)))
18321, 94, 16leaddsub2d 10831 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → (((𝐹𝑖) + 𝐸) ≤ (𝐵𝑖) ↔ 𝐸 ≤ ((𝐵𝑖) − (𝐹𝑖))))
184182, 183mpbird 247 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → ((𝐹𝑖) + 𝐸) ≤ (𝐵𝑖))
1851843ad2antl1 1200 . . . . . . . . . 10 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → ((𝐹𝑖) + 𝐸) ≤ (𝐵𝑖))
18691, 165, 166, 179, 185ltletrd 10399 . . . . . . . . 9 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝑔𝑖) < (𝐵𝑖))
18783, 84, 91, 163, 186eliood 40241 . . . . . . . 8 (((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) ∧ 𝑖𝑋) → (𝑔𝑖) ∈ ((𝐴𝑖)(,)(𝐵𝑖)))
188187ralrimiva 3115 . . . . . . 7 ((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) → ∀𝑖𝑋 (𝑔𝑖) ∈ ((𝐴𝑖)(,)(𝐵𝑖)))
18982, 188jca 501 . . . . . 6 ((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) → (𝑔 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑔𝑖) ∈ ((𝐴𝑖)(,)(𝐵𝑖))))
190 vex 3354 . . . . . . 7 𝑔 ∈ V
191190elixp 8069 . . . . . 6 (𝑔X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)) ↔ (𝑔 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑔𝑖) ∈ ((𝐴𝑖)(,)(𝐵𝑖))))
192189, 191sylibr 224 . . . . 5 ((𝜑𝑔 ∈ (ℝ ↑𝑚 𝑋) ∧ (𝐹𝐷𝑔) < 𝐸) → 𝑔X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))
19380, 75, 11, 61, 192ballss3 39791 . . . 4 (𝜑 → (𝐹(ball‘𝐷)𝐸) ⊆ X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))
19466, 193eqsstrd 3788 . . 3 (𝜑𝑉X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))
19579, 194jca 501 . 2 (𝜑 → (𝐹𝑉𝑉X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖))))
196 eleq2 2839 . . . 4 (𝑣 = 𝑉 → (𝐹𝑣𝐹𝑉))
197 sseq1 3775 . . . 4 (𝑣 = 𝑉 → (𝑣X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)) ↔ 𝑉X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖))))
198196, 197anbi12d 616 . . 3 (𝑣 = 𝑉 → ((𝐹𝑣𝑣X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖))) ↔ (𝐹𝑉𝑉X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))))
199198rspcev 3460 . 2 ((𝑉 ∈ (TopOpen‘(ℝ^‘𝑋)) ∧ (𝐹𝑉𝑉X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))) → ∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝐹𝑣𝑣X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖))))
20073, 195, 199syl2anc 573 1 (𝜑 → ∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝐹𝑣𝑣X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wcel 2145  wne 2943  wral 3061  wrex 3062  Vcvv 3351  wss 3723  c0 4063  ifcif 4225   ciun 4654   class class class wbr 4786  cmpt 4863   Or wor 5169  ran crn 5250   Fn wfn 6026  wf 6027  cfv 6031  (class class class)co 6793  cmpt2 6795  𝑚 cmap 8009  Xcixp 8062  Fincfn 8109  infcinf 8503  cr 10137  0cc0 10138   + caddc 10141  *cxr 10275   < clt 10276  cle 10277  cmin 10468  2c2 11272  +crp 12035  (,)cioo 12380  cexp 13067  csqrt 14181  abscabs 14182  Σcsu 14624  distcds 16158  TopOpenctopn 16290  PsMetcpsmet 19945  ∞Metcxmt 19946  Metcme 19947  ballcbl 19948  MetOpencmopn 19951  ℝ^crrx 23390
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-inf2 8702  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215  ax-pre-sup 10216  ax-addf 10217  ax-mulf 10218
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-fal 1637  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-of 7044  df-om 7213  df-1st 7315  df-2nd 7316  df-supp 7447  df-tpos 7504  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-oadd 7717  df-er 7896  df-map 8011  df-ixp 8063  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-fsupp 8432  df-sup 8504  df-inf 8505  df-oi 8571  df-card 8965  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-2 11281  df-3 11282  df-4 11283  df-5 11284  df-6 11285  df-7 11286  df-8 11287  df-9 11288  df-n0 11495  df-z 11580  df-dec 11696  df-uz 11889  df-q 11992  df-rp 12036  df-xneg 12151  df-xadd 12152  df-xmul 12153  df-ioo 12384  df-ico 12386  df-fz 12534  df-fzo 12674  df-seq 13009  df-exp 13068  df-hash 13322  df-cj 14047  df-re 14048  df-im 14049  df-sqrt 14183  df-abs 14184  df-clim 14427  df-sum 14625  df-struct 16066  df-ndx 16067  df-slot 16068  df-base 16070  df-sets 16071  df-ress 16072  df-plusg 16162  df-mulr 16163  df-starv 16164  df-sca 16165  df-vsca 16166  df-ip 16167  df-tset 16168  df-ple 16169  df-ds 16172  df-unif 16173  df-hom 16174  df-cco 16175  df-rest 16291  df-topn 16292  df-0g 16310  df-gsum 16311  df-topgen 16312  df-prds 16316  df-pws 16318  df-mgm 17450  df-sgrp 17492  df-mnd 17503  df-mhm 17543  df-grp 17633  df-minusg 17634  df-sbg 17635  df-subg 17799  df-ghm 17866  df-cntz 17957  df-cmn 18402  df-abl 18403  df-mgp 18698  df-ur 18710  df-ring 18757  df-cring 18758  df-oppr 18831  df-dvdsr 18849  df-unit 18850  df-invr 18880  df-dvr 18891  df-rnghom 18925  df-drng 18959  df-field 18960  df-subrg 18988  df-staf 19055  df-srng 19056  df-lmod 19075  df-lss 19143  df-sra 19387  df-rgmod 19388  df-psmet 19953  df-xmet 19954  df-met 19955  df-bl 19956  df-mopn 19957  df-cnfld 19962  df-refld 20168  df-dsmm 20293  df-frlm 20308  df-top 20919  df-topon 20936  df-bases 20971  df-nm 22607  df-tng 22609  df-tch 23188  df-rrx 23392
This theorem is referenced by:  ioorrnopn  41042
  Copyright terms: Public domain W3C validator