Metamath Proof Explorer

Theorem ioorrnopn

Description: The indexed product of open intervals is an open set in ( RR^X ) . (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses ioorrnopn.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
ioorrnopn.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
ioorrnopn.b ⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
Assertion ioorrnopn ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 ioorrnopn.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
2 ioorrnopn.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
3 ioorrnopn.b ⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
4 p0ex ⊢ { ∅ } ∈ V
5 4 prid2 ⊢ { ∅ } ∈ { ∅ , { ∅ } }
6 5 a1i ⊢ ( 𝑋 = ∅ → { ∅ } ∈ { ∅ , { ∅ } } )
7 ixpeq1 ⊢ ( 𝑋 = ∅ → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) = X 𝑖 ∈ ∅ ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) )
8 ixp0x ⊢ X 𝑖 ∈ ∅ ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) = { ∅ }
9 8 a1i ⊢ ( 𝑋 = ∅ → X 𝑖 ∈ ∅ ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) = { ∅ } )
10 7 9 eqtrd ⊢ ( 𝑋 = ∅ → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) = { ∅ } )
11 2fveq3 ⊢ ( 𝑋 = ∅ → ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) = ( TopOpen ‘ ( ℝ^ ‘ ∅ ) ) )
12 rrxtopn0b ⊢ ( TopOpen ‘ ( ℝ^ ‘ ∅ ) ) = { ∅ , { ∅ } }
13 12 a1i ⊢ ( 𝑋 = ∅ → ( TopOpen ‘ ( ℝ^ ‘ ∅ ) ) = { ∅ , { ∅ } } )
14 11 13 eqtrd ⊢ ( 𝑋 = ∅ → ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) = { ∅ , { ∅ } } )
15 10 14 eleq12d ⊢ ( 𝑋 = ∅ → ( X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ↔ { ∅ } ∈ { ∅ , { ∅ } } ) )
16 6 15 mpbird ⊢ ( 𝑋 = ∅ → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) )
18 neqne ⊢ ( ¬ 𝑋 = ∅ → 𝑋 ≠ ∅ )
19 18 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → 𝑋 ≠ ∅ )
20 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝐴 ‘ 𝑖 ) = ( 𝐴 ‘ 𝑗 ) )
21 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝐵 ‘ 𝑖 ) = ( 𝐵 ‘ 𝑗 ) )
22 20 21 oveq12d ⊢ ( 𝑖 = 𝑗 → ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) = ( ( 𝐴 ‘ 𝑗 ) (,) ( 𝐵 ‘ 𝑗 ) ) )
23 22 cbvixpv ⊢ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) = X 𝑗 ∈ 𝑋 ( ( 𝐴 ‘ 𝑗 ) (,) ( 𝐵 ‘ 𝑗 ) )
24 23 eleq2i ⊢ ( 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ↔ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐴 ‘ 𝑗 ) (,) ( 𝐵 ‘ 𝑗 ) ) )
25 24 biimpi ⊢ ( 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) → 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐴 ‘ 𝑗 ) (,) ( 𝐵 ‘ 𝑗 ) ) )
26 25 adantl ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) → 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐴 ‘ 𝑗 ) (,) ( 𝐵 ‘ 𝑗 ) ) )
27 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) → 𝑋 ∈ Fin )
28 24 27 sylan2br ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐴 ‘ 𝑗 ) (,) ( 𝐵 ‘ 𝑗 ) ) ) → 𝑋 ∈ Fin )
29 simplr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) → 𝑋 ≠ ∅ )
30 24 29 sylan2br ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐴 ‘ 𝑗 ) (,) ( 𝐵 ‘ 𝑗 ) ) ) → 𝑋 ≠ ∅ )
31 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) → 𝐴 : 𝑋 ⟶ ℝ )
32 24 31 sylan2br ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐴 ‘ 𝑗 ) (,) ( 𝐵 ‘ 𝑗 ) ) ) → 𝐴 : 𝑋 ⟶ ℝ )
33 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) → 𝐵 : 𝑋 ⟶ ℝ )
34 24 33 sylan2br ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐴 ‘ 𝑗 ) (,) ( 𝐵 ‘ 𝑗 ) ) ) → 𝐵 : 𝑋 ⟶ ℝ )
35 simpr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) → 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) )
36 24 35 sylan2br ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐴 ‘ 𝑗 ) (,) ( 𝐵 ‘ 𝑗 ) ) ) → 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) )
37 eqid ⊢ ran ( 𝑖 ∈ 𝑋 ↦ if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ≤ ( ( 𝑓 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) , ( ( 𝑓 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) = ran ( 𝑖 ∈ 𝑋 ↦ if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ≤ ( ( 𝑓 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) , ( ( 𝑓 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) )
38 fveq2 ⊢ ( 𝑗 = 𝑖 → ( 𝐵 ‘ 𝑗 ) = ( 𝐵 ‘ 𝑖 ) )
39 fveq2 ⊢ ( 𝑗 = 𝑖 → ( 𝑓 ‘ 𝑗 ) = ( 𝑓 ‘ 𝑖 ) )
40 38 39 oveq12d ⊢ ( 𝑗 = 𝑖 → ( ( 𝐵 ‘ 𝑗 ) − ( 𝑓 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) )
41 fveq2 ⊢ ( 𝑗 = 𝑖 → ( 𝐴 ‘ 𝑗 ) = ( 𝐴 ‘ 𝑖 ) )
42 39 41 oveq12d ⊢ ( 𝑗 = 𝑖 → ( ( 𝑓 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝑓 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) )
43 40 42 breq12d ⊢ ( 𝑗 = 𝑖 → ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝑓 ‘ 𝑗 ) ) ≤ ( ( 𝑓 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ↔ ( ( 𝐵 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ≤ ( ( 𝑓 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) )
44 43 40 42 ifbieq12d ⊢ ( 𝑗 = 𝑖 → if ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝑓 ‘ 𝑗 ) ) ≤ ( ( 𝑓 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) , ( ( 𝐵 ‘ 𝑗 ) − ( 𝑓 ‘ 𝑗 ) ) , ( ( 𝑓 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ≤ ( ( 𝑓 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) , ( ( 𝑓 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) )
45 44 cbvmptv ⊢ ( 𝑗 ∈ 𝑋 ↦ if ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝑓 ‘ 𝑗 ) ) ≤ ( ( 𝑓 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) , ( ( 𝐵 ‘ 𝑗 ) − ( 𝑓 ‘ 𝑗 ) ) , ( ( 𝑓 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) ) = ( 𝑖 ∈ 𝑋 ↦ if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ≤ ( ( 𝑓 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) , ( ( 𝑓 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) )
46 45 rneqi ⊢ ran ( 𝑗 ∈ 𝑋 ↦ if ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝑓 ‘ 𝑗 ) ) ≤ ( ( 𝑓 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) , ( ( 𝐵 ‘ 𝑗 ) − ( 𝑓 ‘ 𝑗 ) ) , ( ( 𝑓 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) ) = ran ( 𝑖 ∈ 𝑋 ↦ if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ≤ ( ( 𝑓 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) , ( ( 𝑓 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) )
47 46 infeq1i ⊢ inf ( ran ( 𝑗 ∈ 𝑋 ↦ if ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝑓 ‘ 𝑗 ) ) ≤ ( ( 𝑓 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) , ( ( 𝐵 ‘ 𝑗 ) − ( 𝑓 ‘ 𝑗 ) ) , ( ( 𝑓 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) ) , ℝ , < ) = inf ( ran ( 𝑖 ∈ 𝑋 ↦ if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ≤ ( ( 𝑓 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) , ( ( 𝑓 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) , ℝ , < )
48 eqid ⊢ ( 𝑓 ( ball ‘ ( 𝑎 ∈ ( ℝ ↑m 𝑋 ) , 𝑏 ∈ ( ℝ ↑m 𝑋 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝑋 ( ( ( 𝑎 ‘ 𝑘 ) − ( 𝑏 ‘ 𝑘 ) ) ↑ 2 ) ) ) ) inf ( ran ( 𝑗 ∈ 𝑋 ↦ if ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝑓 ‘ 𝑗 ) ) ≤ ( ( 𝑓 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) , ( ( 𝐵 ‘ 𝑗 ) − ( 𝑓 ‘ 𝑗 ) ) , ( ( 𝑓 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) ) , ℝ , < ) ) = ( 𝑓 ( ball ‘ ( 𝑎 ∈ ( ℝ ↑m 𝑋 ) , 𝑏 ∈ ( ℝ ↑m 𝑋 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝑋 ( ( ( 𝑎 ‘ 𝑘 ) − ( 𝑏 ‘ 𝑘 ) ) ↑ 2 ) ) ) ) inf ( ran ( 𝑗 ∈ 𝑋 ↦ if ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝑓 ‘ 𝑗 ) ) ≤ ( ( 𝑓 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) , ( ( 𝐵 ‘ 𝑗 ) − ( 𝑓 ‘ 𝑗 ) ) , ( ( 𝑓 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) ) , ℝ , < ) )
49 fveq1 ⊢ ( 𝑎 = 𝑔 → ( 𝑎 ‘ 𝑘 ) = ( 𝑔 ‘ 𝑘 ) )
50 49 oveq1d ⊢ ( 𝑎 = 𝑔 → ( ( 𝑎 ‘ 𝑘 ) − ( 𝑏 ‘ 𝑘 ) ) = ( ( 𝑔 ‘ 𝑘 ) − ( 𝑏 ‘ 𝑘 ) ) )
51 50 oveq1d ⊢ ( 𝑎 = 𝑔 → ( ( ( 𝑎 ‘ 𝑘 ) − ( 𝑏 ‘ 𝑘 ) ) ↑ 2 ) = ( ( ( 𝑔 ‘ 𝑘 ) − ( 𝑏 ‘ 𝑘 ) ) ↑ 2 ) )
52 51 sumeq2sdv ⊢ ( 𝑎 = 𝑔 → Σ 𝑘 ∈ 𝑋 ( ( ( 𝑎 ‘ 𝑘 ) − ( 𝑏 ‘ 𝑘 ) ) ↑ 2 ) = Σ 𝑘 ∈ 𝑋 ( ( ( 𝑔 ‘ 𝑘 ) − ( 𝑏 ‘ 𝑘 ) ) ↑ 2 ) )
53 52 fveq2d ⊢ ( 𝑎 = 𝑔 → ( √ ‘ Σ 𝑘 ∈ 𝑋 ( ( ( 𝑎 ‘ 𝑘 ) − ( 𝑏 ‘ 𝑘 ) ) ↑ 2 ) ) = ( √ ‘ Σ 𝑘 ∈ 𝑋 ( ( ( 𝑔 ‘ 𝑘 ) − ( 𝑏 ‘ 𝑘 ) ) ↑ 2 ) ) )
54 fveq1 ⊢ ( 𝑏 = ℎ → ( 𝑏 ‘ 𝑘 ) = ( ℎ ‘ 𝑘 ) )
55 54 oveq2d ⊢ ( 𝑏 = ℎ → ( ( 𝑔 ‘ 𝑘 ) − ( 𝑏 ‘ 𝑘 ) ) = ( ( 𝑔 ‘ 𝑘 ) − ( ℎ ‘ 𝑘 ) ) )
56 55 oveq1d ⊢ ( 𝑏 = ℎ → ( ( ( 𝑔 ‘ 𝑘 ) − ( 𝑏 ‘ 𝑘 ) ) ↑ 2 ) = ( ( ( 𝑔 ‘ 𝑘 ) − ( ℎ ‘ 𝑘 ) ) ↑ 2 ) )
57 56 sumeq2sdv ⊢ ( 𝑏 = ℎ → Σ 𝑘 ∈ 𝑋 ( ( ( 𝑔 ‘ 𝑘 ) − ( 𝑏 ‘ 𝑘 ) ) ↑ 2 ) = Σ 𝑘 ∈ 𝑋 ( ( ( 𝑔 ‘ 𝑘 ) − ( ℎ ‘ 𝑘 ) ) ↑ 2 ) )
58 57 fveq2d ⊢ ( 𝑏 = ℎ → ( √ ‘ Σ 𝑘 ∈ 𝑋 ( ( ( 𝑔 ‘ 𝑘 ) − ( 𝑏 ‘ 𝑘 ) ) ↑ 2 ) ) = ( √ ‘ Σ 𝑘 ∈ 𝑋 ( ( ( 𝑔 ‘ 𝑘 ) − ( ℎ ‘ 𝑘 ) ) ↑ 2 ) ) )
59 53 58 cbvmpov ⊢ ( 𝑎 ∈ ( ℝ ↑m 𝑋 ) , 𝑏 ∈ ( ℝ ↑m 𝑋 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝑋 ( ( ( 𝑎 ‘ 𝑘 ) − ( 𝑏 ‘ 𝑘 ) ) ↑ 2 ) ) ) = ( 𝑔 ∈ ( ℝ ↑m 𝑋 ) , ℎ ∈ ( ℝ ↑m 𝑋 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝑋 ( ( ( 𝑔 ‘ 𝑘 ) − ( ℎ ‘ 𝑘 ) ) ↑ 2 ) ) )
60 28 30 32 34 36 37 47 48 59 ioorrnopnlem ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐴 ‘ 𝑗 ) (,) ( 𝐵 ‘ 𝑗 ) ) ) → ∃ 𝑣 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ( 𝑓 ∈ 𝑣 ∧ 𝑣 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) )
61 26 60 syldan ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) → ∃ 𝑣 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ( 𝑓 ∈ 𝑣 ∧ 𝑣 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) )
62 61 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ∀ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∃ 𝑣 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ( 𝑓 ∈ 𝑣 ∧ 𝑣 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) )
63 eqid ⊢ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) = ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) )
64 63 rrxtop ⊢ ( 𝑋 ∈ Fin → ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ∈ Top )
65 1 64 syl ⊢ ( 𝜑 → ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ∈ Top )
66 65 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ∈ Top )
67 eltop2 ⊢ ( ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ∈ Top → ( X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ↔ ∀ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∃ 𝑣 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ( 𝑓 ∈ 𝑣 ∧ 𝑣 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) ) )
68 66 67 syl ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ↔ ∀ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∃ 𝑣 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ( 𝑓 ∈ 𝑣 ∧ 𝑣 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) ) )
69 62 68 mpbird ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) )
70 19 69 syldan ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) )
71 17 70 pm2.61dan ⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) )