Metamath Proof Explorer

Theorem ioorrnopnlem

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)

Ref Expression
Hypotheses 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 ioorrnopnlem ( 𝜑 → ∃ 𝑣 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ( 𝐹 ∈ 𝑣 ∧ 𝑣 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) )

Proof

Step Hyp Ref Expression
1 ioorrnopnlem.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
2 ioorrnopnlem.n ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
3 ioorrnopnlem.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
4 ioorrnopnlem.b ⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
5 ioorrnopnlem.f ⊢ ( 𝜑 → 𝐹 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) )
6 ioorrnopnlem.h ⊢ 𝐻 = ran ( 𝑖 ∈ 𝑋 ↦ if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) )
7 ioorrnopnlem.e ⊢ 𝐸 = inf ( 𝐻 , ℝ , < )
8 ioorrnopnlem.v ⊢ 𝑉 = ( 𝐹 ( ball ‘ 𝐷 ) 𝐸 )
9 ioorrnopnlem.d ⊢ 𝐷 = ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) , 𝑔 ∈ ( ℝ ↑m 𝑋 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝑋 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) )
10 1 9 rrndsxmet ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ ( ℝ ↑m 𝑋 ) ) )
11 nfv ⊢ Ⅎ 𝑖 𝜑
12 reex ⊢ ℝ ∈ V
13 12 a1i ⊢ ( 𝜑 → ℝ ∈ V )
14 ioossre ⊢ ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ⊆ ℝ
15 14 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ⊆ ℝ )
16 11 13 15 ixpssmapc ⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ⊆ ( ℝ ↑m 𝑋 ) )
17 16 5 sseldd ⊢ ( 𝜑 → 𝐹 ∈ ( ℝ ↑m 𝑋 ) )
18 6 a1i ⊢ ( 𝜑 → 𝐻 = ran ( 𝑖 ∈ 𝑋 ↦ if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) )
19 4 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ )
20 5 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 𝐹 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) )
21 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ 𝑋 )
22 fvixp2 ⊢ ( ( 𝐹 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑖 ) ∈ ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) )
23 20 21 22 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑖 ) ∈ ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) )
24 14 23 sseldi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑖 ) ∈ ℝ )
25 19 24 resubcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ∈ ℝ )
26 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑖 ) ∈ ℝ )
27 26 rexrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑖 ) ∈ ℝ* )
28 19 rexrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ* )
29 iooltub ⊢ ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝐹 ‘ 𝑖 ) ∈ ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) → ( 𝐹 ‘ 𝑖 ) < ( 𝐵 ‘ 𝑖 ) )
30 27 28 23 29 syl3anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑖 ) < ( 𝐵 ‘ 𝑖 ) )
31 24 19 posdifd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑖 ) < ( 𝐵 ‘ 𝑖 ) ↔ 0 < ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ) )
32 30 31 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 0 < ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) )
33 25 32 elrpd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ∈ ℝ+ )
34 24 26 resubcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ∈ ℝ )
35 ioogtlb ⊢ ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝐹 ‘ 𝑖 ) ∈ ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) → ( 𝐴 ‘ 𝑖 ) < ( 𝐹 ‘ 𝑖 ) )
36 27 28 23 35 syl3anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑖 ) < ( 𝐹 ‘ 𝑖 ) )
37 26 24 posdifd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐴 ‘ 𝑖 ) < ( 𝐹 ‘ 𝑖 ) ↔ 0 < ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) )
38 36 37 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 0 < ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) )
39 34 38 elrpd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ∈ ℝ+ )
40 33 39 ifcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ∈ ℝ+ )
41 40 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝑋 if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ∈ ℝ+ )
42 eqid ⊢ ( 𝑖 ∈ 𝑋 ↦ if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) = ( 𝑖 ∈ 𝑋 ↦ if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) )
43 42 rnmptss ⊢ ( ∀ 𝑖 ∈ 𝑋 if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ∈ ℝ+ → ran ( 𝑖 ∈ 𝑋 ↦ if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ⊆ ℝ+ )
44 41 43 syl ⊢ ( 𝜑 → ran ( 𝑖 ∈ 𝑋 ↦ if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ⊆ ℝ+ )
45 18 44 eqsstrd ⊢ ( 𝜑 → 𝐻 ⊆ ℝ+ )
46 ltso ⊢ < Or ℝ
47 46 a1i ⊢ ( 𝜑 → < Or ℝ )
48 42 rnmptfi ⊢ ( 𝑋 ∈ Fin → ran ( 𝑖 ∈ 𝑋 ↦ if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ∈ Fin )
49 1 48 syl ⊢ ( 𝜑 → ran ( 𝑖 ∈ 𝑋 ↦ if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ∈ Fin )
50 6 49 eqeltrid ⊢ ( 𝜑 → 𝐻 ∈ Fin )
51 40 elexd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ∈ V )
52 11 51 42 2 rnmptn0 ⊢ ( 𝜑 → ran ( 𝑖 ∈ 𝑋 ↦ if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ≠ ∅ )
53 18 52 eqnetrd ⊢ ( 𝜑 → 𝐻 ≠ ∅ )
54 rpssre ⊢ ℝ+ ⊆ ℝ
55 54 a1i ⊢ ( 𝜑 → ℝ+ ⊆ ℝ )
56 45 55 sstrd ⊢ ( 𝜑 → 𝐻 ⊆ ℝ )
57 fiinfcl ⊢ ( ( < Or ℝ ∧ ( 𝐻 ∈ Fin ∧ 𝐻 ≠ ∅ ∧ 𝐻 ⊆ ℝ ) ) → inf ( 𝐻 , ℝ , < ) ∈ 𝐻 )
58 47 50 53 56 57 syl13anc ⊢ ( 𝜑 → inf ( 𝐻 , ℝ , < ) ∈ 𝐻 )
59 45 58 sseldd ⊢ ( 𝜑 → inf ( 𝐻 , ℝ , < ) ∈ ℝ+ )
60 7 59 eqeltrid ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
61 rpxr ⊢ ( 𝐸 ∈ ℝ+ → 𝐸 ∈ ℝ* )
62 60 61 syl ⊢ ( 𝜑 → 𝐸 ∈ ℝ* )
63 eqid ⊢ ( MetOpen ‘ 𝐷 ) = ( MetOpen ‘ 𝐷 )
64 63 blopn ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ ( ℝ ↑m 𝑋 ) ) ∧ 𝐹 ∈ ( ℝ ↑m 𝑋 ) ∧ 𝐸 ∈ ℝ* ) → ( 𝐹 ( ball ‘ 𝐷 ) 𝐸 ) ∈ ( MetOpen ‘ 𝐷 ) )
65 10 17 62 64 syl3anc ⊢ ( 𝜑 → ( 𝐹 ( ball ‘ 𝐷 ) 𝐸 ) ∈ ( MetOpen ‘ 𝐷 ) )
66 8 a1i ⊢ ( 𝜑 → 𝑉 = ( 𝐹 ( ball ‘ 𝐷 ) 𝐸 ) )
67 1 rrxtopnfi ⊢ ( 𝜑 → ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) = ( MetOpen ‘ ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) , 𝑔 ∈ ( ℝ ↑m 𝑋 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝑋 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) ) )
68 9 eqcomi ⊢ ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) , 𝑔 ∈ ( ℝ ↑m 𝑋 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝑋 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) = 𝐷
69 68 a1i ⊢ ( 𝜑 → ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) , 𝑔 ∈ ( ℝ ↑m 𝑋 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝑋 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) = 𝐷 )
70 69 fveq2d ⊢ ( 𝜑 → ( MetOpen ‘ ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) , 𝑔 ∈ ( ℝ ↑m 𝑋 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝑋 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) ) = ( MetOpen ‘ 𝐷 ) )
71 67 70 eqtrd ⊢ ( 𝜑 → ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) = ( MetOpen ‘ 𝐷 ) )
72 66 71 eleq12d ⊢ ( 𝜑 → ( 𝑉 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ↔ ( 𝐹 ( ball ‘ 𝐷 ) 𝐸 ) ∈ ( MetOpen ‘ 𝐷 ) ) )
73 65 72 mpbird ⊢ ( 𝜑 → 𝑉 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) )
74 xmetpsmet ⊢ ( 𝐷 ∈ ( ∞Met ‘ ( ℝ ↑m 𝑋 ) ) → 𝐷 ∈ ( PsMet ‘ ( ℝ ↑m 𝑋 ) ) )
75 10 74 syl ⊢ ( 𝜑 → 𝐷 ∈ ( PsMet ‘ ( ℝ ↑m 𝑋 ) ) )
76 blcntrps ⊢ ( ( 𝐷 ∈ ( PsMet ‘ ( ℝ ↑m 𝑋 ) ) ∧ 𝐹 ∈ ( ℝ ↑m 𝑋 ) ∧ 𝐸 ∈ ℝ+ ) → 𝐹 ∈ ( 𝐹 ( ball ‘ 𝐷 ) 𝐸 ) )
77 75 17 60 76 syl3anc ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐹 ( ball ‘ 𝐷 ) 𝐸 ) )
78 66 eqcomd ⊢ ( 𝜑 → ( 𝐹 ( ball ‘ 𝐷 ) 𝐸 ) = 𝑉 )
79 77 78 eleqtrd ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
80 nfv ⊢ Ⅎ 𝑔 𝜑
81 elmapfn ⊢ ( 𝑔 ∈ ( ℝ ↑m 𝑋 ) → 𝑔 Fn 𝑋 )
82 81 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) → 𝑔 Fn 𝑋 )
83 27 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑖 ) ∈ ℝ* )
84 28 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ* )
85 simpl2 ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) ∧ 𝑖 ∈ 𝑋 ) → 𝑔 ∈ ( ℝ ↑m 𝑋 ) )
86 simpr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ 𝑋 )
87 elmapi ⊢ ( 𝑔 ∈ ( ℝ ↑m 𝑋 ) → 𝑔 : 𝑋 ⟶ ℝ )
88 87 adantr ⊢ ( ( 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ 𝑖 ∈ 𝑋 ) → 𝑔 : 𝑋 ⟶ ℝ )
89 simpr ⊢ ( ( 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ 𝑋 )
90 88 89 ffvelrnd ⊢ ( ( 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑔 ‘ 𝑖 ) ∈ ℝ )
91 85 86 90 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑔 ‘ 𝑖 ) ∈ ℝ )
92 26 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑖 ) ∈ ℝ )
93 54 60 sseldi ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
94 93 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 𝐸 ∈ ℝ )
95 24 94 resubcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑖 ) − 𝐸 ) ∈ ℝ )
96 95 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑖 ) − 𝐸 ) ∈ ℝ )
97 54 40 sseldi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ∈ ℝ )
98 7 a1i ⊢ ( 𝜑 → 𝐸 = inf ( 𝐻 , ℝ , < ) )
99 infxrrefi ⊢ ( ( 𝐻 ⊆ ℝ ∧ 𝐻 ∈ Fin ∧ 𝐻 ≠ ∅ ) → inf ( 𝐻 , ℝ* , < ) = inf ( 𝐻 , ℝ , < ) )
100 56 50 53 99 syl3anc ⊢ ( 𝜑 → inf ( 𝐻 , ℝ* , < ) = inf ( 𝐻 , ℝ , < ) )
101 100 eqcomd ⊢ ( 𝜑 → inf ( 𝐻 , ℝ , < ) = inf ( 𝐻 , ℝ* , < ) )
102 98 101 eqtrd ⊢ ( 𝜑 → 𝐸 = inf ( 𝐻 , ℝ* , < ) )
103 102 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 𝐸 = inf ( 𝐻 , ℝ* , < ) )
104 ressxr ⊢ ℝ ⊆ ℝ*
105 104 a1i ⊢ ( 𝜑 → ℝ ⊆ ℝ* )
106 56 105 sstrd ⊢ ( 𝜑 → 𝐻 ⊆ ℝ* )
107 106 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 𝐻 ⊆ ℝ* )
108 42 elrnmpt1 ⊢ ( ( 𝑖 ∈ 𝑋 ∧ if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ∈ V ) → if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ∈ ran ( 𝑖 ∈ 𝑋 ↦ if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) )
109 21 51 108 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ∈ ran ( 𝑖 ∈ 𝑋 ↦ if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) )
110 109 6 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ∈ 𝐻 )
111 infxrlb ⊢ ( ( 𝐻 ⊆ ℝ* ∧ if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ∈ 𝐻 ) → inf ( 𝐻 , ℝ* , < ) ≤ if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) )
112 107 110 111 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → inf ( 𝐻 , ℝ* , < ) ≤ if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) )
113 103 112 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 𝐸 ≤ if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) )
114 min2 ⊢ ( ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ∈ ℝ ) → if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) )
115 25 34 114 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) )
116 94 97 34 113 115 letrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 𝐸 ≤ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) )
117 94 24 26 116 lesubd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑖 ) ≤ ( ( 𝐹 ‘ 𝑖 ) − 𝐸 ) )
118 117 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑖 ) ≤ ( ( 𝐹 ‘ 𝑖 ) − 𝐸 ) )
119 24 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑖 ) ∈ ℝ )
120 90 adantll ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑔 ‘ 𝑖 ) ∈ ℝ )
121 119 120 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑖 ) − ( 𝑔 ‘ 𝑖 ) ) ∈ ℝ )
122 121 3adantl3 ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑖 ) − ( 𝑔 ‘ 𝑖 ) ) ∈ ℝ )
123 1 9 rrndsmet ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ ( ℝ ↑m 𝑋 ) ) )
124 123 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝐷 ∈ ( Met ‘ ( ℝ ↑m 𝑋 ) ) )
125 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝐹 ∈ ( ℝ ↑m 𝑋 ) )
126 simplr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑔 ∈ ( ℝ ↑m 𝑋 ) )
127 metcl ⊢ ( ( 𝐷 ∈ ( Met ‘ ( ℝ ↑m 𝑋 ) ) ∧ 𝐹 ∈ ( ℝ ↑m 𝑋 ) ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ) → ( 𝐹 𝐷 𝑔 ) ∈ ℝ )
128 124 125 126 127 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐹 𝐷 𝑔 ) ∈ ℝ )
129 128 3adantl3 ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐹 𝐷 𝑔 ) ∈ ℝ )
130 94 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝐸 ∈ ℝ )
131 130 3adantl3 ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) ∧ 𝑖 ∈ 𝑋 ) → 𝐸 ∈ ℝ )
132 121 recnd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑖 ) − ( 𝑔 ‘ 𝑖 ) ) ∈ ℂ )
133 132 abscld ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝑔 ‘ 𝑖 ) ) ) ∈ ℝ )
134 121 leabsd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑖 ) − ( 𝑔 ‘ 𝑖 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝑔 ‘ 𝑖 ) ) ) )
135 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑋 ∈ Fin )
136 ixpf ⊢ ( 𝐹 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) → 𝐹 : 𝑋 ⟶ ∪ 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) )
137 5 136 syl ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ∪ 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) )
138 15 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ⊆ ℝ )
139 iunss ⊢ ( ∪ 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ⊆ ℝ ↔ ∀ 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ⊆ ℝ )
140 138 139 sylibr ⊢ ( 𝜑 → ∪ 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ⊆ ℝ )
141 137 140 fssd ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℝ )
142 141 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝐹 : 𝑋 ⟶ ℝ )
143 126 87 syl ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑔 : 𝑋 ⟶ ℝ )
144 simpr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ 𝑋 )
145 eqid ⊢ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) = ( dist ‘ ( ℝ^ ‘ 𝑋 ) )
146 135 142 143 144 145 rrnprjdstle ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝑔 ‘ 𝑖 ) ) ) ≤ ( 𝐹 ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) 𝑔 ) )
147 eqid ⊢ ( ℝ^ ‘ 𝑋 ) = ( ℝ^ ‘ 𝑋 )
148 eqid ⊢ ( ℝ ↑m 𝑋 ) = ( ℝ ↑m 𝑋 )
149 147 148 rrxdsfi ⊢ ( 𝑋 ∈ Fin → ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) = ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) , 𝑔 ∈ ( ℝ ↑m 𝑋 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝑋 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
150 1 149 syl ⊢ ( 𝜑 → ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) = ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) , 𝑔 ∈ ( ℝ ↑m 𝑋 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝑋 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
151 150 69 eqtrd ⊢ ( 𝜑 → ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) = 𝐷 )
152 151 oveqd ⊢ ( 𝜑 → ( 𝐹 ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) 𝑔 ) = ( 𝐹 𝐷 𝑔 ) )
153 152 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐹 ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) 𝑔 ) = ( 𝐹 𝐷 𝑔 ) )
154 146 153 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝑔 ‘ 𝑖 ) ) ) ≤ ( 𝐹 𝐷 𝑔 ) )
155 121 133 128 134 154 letrd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑖 ) − ( 𝑔 ‘ 𝑖 ) ) ≤ ( 𝐹 𝐷 𝑔 ) )
156 155 3adantl3 ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑖 ) − ( 𝑔 ‘ 𝑖 ) ) ≤ ( 𝐹 𝐷 𝑔 ) )
157 simpl3 ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐹 𝐷 𝑔 ) < 𝐸 )
158 122 129 131 156 157 lelttrd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑖 ) − ( 𝑔 ‘ 𝑖 ) ) < 𝐸 )
159 ltsub23 ⊢ ( ( ( 𝐹 ‘ 𝑖 ) ∈ ℝ ∧ ( 𝑔 ‘ 𝑖 ) ∈ ℝ ∧ 𝐸 ∈ ℝ ) → ( ( ( 𝐹 ‘ 𝑖 ) − ( 𝑔 ‘ 𝑖 ) ) < 𝐸 ↔ ( ( 𝐹 ‘ 𝑖 ) − 𝐸 ) < ( 𝑔 ‘ 𝑖 ) ) )
160 119 120 130 159 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝐹 ‘ 𝑖 ) − ( 𝑔 ‘ 𝑖 ) ) < 𝐸 ↔ ( ( 𝐹 ‘ 𝑖 ) − 𝐸 ) < ( 𝑔 ‘ 𝑖 ) ) )
161 160 3adantl3 ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝐹 ‘ 𝑖 ) − ( 𝑔 ‘ 𝑖 ) ) < 𝐸 ↔ ( ( 𝐹 ‘ 𝑖 ) − 𝐸 ) < ( 𝑔 ‘ 𝑖 ) ) )
162 158 161 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑖 ) − 𝐸 ) < ( 𝑔 ‘ 𝑖 ) )
163 92 96 91 118 162 lelttrd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑖 ) < ( 𝑔 ‘ 𝑖 ) )
164 24 94 readdcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑖 ) + 𝐸 ) ∈ ℝ )
165 164 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑖 ) + 𝐸 ) ∈ ℝ )
166 19 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ )
167 120 119 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑔 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ∈ ℝ )
168 167 3adantl3 ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑔 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ∈ ℝ )
169 167 leabsd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑔 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( abs ‘ ( ( 𝑔 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ) )
170 120 recnd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑔 ‘ 𝑖 ) ∈ ℂ )
171 119 recnd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑖 ) ∈ ℂ )
172 170 171 abssubd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → ( abs ‘ ( ( 𝑔 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝑔 ‘ 𝑖 ) ) ) )
173 169 172 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑔 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑖 ) − ( 𝑔 ‘ 𝑖 ) ) ) )
174 167 133 128 173 154 letrd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑔 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( 𝐹 𝐷 𝑔 ) )
175 174 3adantl3 ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑔 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( 𝐹 𝐷 𝑔 ) )
176 168 129 131 175 157 lelttrd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑔 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) < 𝐸 )
177 119 3adantl3 ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑖 ) ∈ ℝ )
178 91 177 131 ltsubadd2d ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝑔 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) < 𝐸 ↔ ( 𝑔 ‘ 𝑖 ) < ( ( 𝐹 ‘ 𝑖 ) + 𝐸 ) ) )
179 176 178 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑔 ‘ 𝑖 ) < ( ( 𝐹 ‘ 𝑖 ) + 𝐸 ) )
180 min1 ⊢ ( ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ∈ ℝ ) → if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) )
181 25 34 180 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ≤ ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) )
182 94 97 25 113 181 letrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 𝐸 ≤ ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) )
183 24 94 19 leaddsub2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝐹 ‘ 𝑖 ) + 𝐸 ) ≤ ( 𝐵 ‘ 𝑖 ) ↔ 𝐸 ≤ ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ) )
184 182 183 mpbird ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑖 ) + 𝐸 ) ≤ ( 𝐵 ‘ 𝑖 ) )
185 184 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑖 ) + 𝐸 ) ≤ ( 𝐵 ‘ 𝑖 ) )
186 91 165 166 179 185 ltletrd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑔 ‘ 𝑖 ) < ( 𝐵 ‘ 𝑖 ) )
187 83 84 91 163 186 eliood ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑔 ‘ 𝑖 ) ∈ ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) )
188 187 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) → ∀ 𝑖 ∈ 𝑋 ( 𝑔 ‘ 𝑖 ) ∈ ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) )
189 82 188 jca ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) → ( 𝑔 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑔 ‘ 𝑖 ) ∈ ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) )
190 vex ⊢ 𝑔 ∈ V
191 190 elixp ⊢ ( 𝑔 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ↔ ( 𝑔 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑔 ‘ 𝑖 ) ∈ ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) )
192 189 191 sylibr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ℝ ↑m 𝑋 ) ∧ ( 𝐹 𝐷 𝑔 ) < 𝐸 ) → 𝑔 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) )
193 80 75 17 62 192 ballss3 ⊢ ( 𝜑 → ( 𝐹 ( ball ‘ 𝐷 ) 𝐸 ) ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) )
194 66 193 eqsstrd ⊢ ( 𝜑 → 𝑉 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) )
195 79 194 jca ⊢ ( 𝜑 → ( 𝐹 ∈ 𝑉 ∧ 𝑉 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) )
196 eleq2 ⊢ ( 𝑣 = 𝑉 → ( 𝐹 ∈ 𝑣 ↔ 𝐹 ∈ 𝑉 ) )
197 sseq1 ⊢ ( 𝑣 = 𝑉 → ( 𝑣 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ↔ 𝑉 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) )
198 196 197 anbi12d ⊢ ( 𝑣 = 𝑉 → ( ( 𝐹 ∈ 𝑣 ∧ 𝑣 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) ↔ ( 𝐹 ∈ 𝑉 ∧ 𝑉 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) ) )
199 198 rspcev ⊢ ( ( 𝑉 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝑉 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) ) → ∃ 𝑣 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ( 𝐹 ∈ 𝑣 ∧ 𝑣 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) )
200 73 195 199 syl2anc ⊢ ( 𝜑 → ∃ 𝑣 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ( 𝐹 ∈ 𝑣 ∧ 𝑣 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) )