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 bilani ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) → 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐴 ‘ 𝑗 ) (,) ( 𝐵 ‘ 𝑗 ) ) )
26 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) → 𝑋 ∈ Fin )
27 24 26 sylan2br ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐴 ‘ 𝑗 ) (,) ( 𝐵 ‘ 𝑗 ) ) ) → 𝑋 ∈ Fin )
28 simplr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) → 𝑋 ≠ ∅ )
29 24 28 sylan2br ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐴 ‘ 𝑗 ) (,) ( 𝐵 ‘ 𝑗 ) ) ) → 𝑋 ≠ ∅ )
30 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) → 𝐴 : 𝑋 ⟶ ℝ )
31 24 30 sylan2br ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐴 ‘ 𝑗 ) (,) ( 𝐵 ‘ 𝑗 ) ) ) → 𝐴 : 𝑋 ⟶ ℝ )
32 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) → 𝐵 : 𝑋 ⟶ ℝ )
33 24 32 sylan2br ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐴 ‘ 𝑗 ) (,) ( 𝐵 ‘ 𝑗 ) ) ) → 𝐵 : 𝑋 ⟶ ℝ )
34 24 bilanri ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐴 ‘ 𝑗 ) (,) ( 𝐵 ‘ 𝑗 ) ) ) → 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) )
35 eqid ⊢ ran ( 𝑖 ∈ 𝑋 ↦ if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ≤ ( ( 𝑓 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) , ( ( 𝑓 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) = ran ( 𝑖 ∈ 𝑋 ↦ if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ≤ ( ( 𝑓 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) , ( ( 𝑓 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) )
36 fveq2 ⊢ ( 𝑗 = 𝑖 → ( 𝐵 ‘ 𝑗 ) = ( 𝐵 ‘ 𝑖 ) )
37 fveq2 ⊢ ( 𝑗 = 𝑖 → ( 𝑓 ‘ 𝑗 ) = ( 𝑓 ‘ 𝑖 ) )
38 36 37 oveq12d ⊢ ( 𝑗 = 𝑖 → ( ( 𝐵 ‘ 𝑗 ) − ( 𝑓 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) )
39 fveq2 ⊢ ( 𝑗 = 𝑖 → ( 𝐴 ‘ 𝑗 ) = ( 𝐴 ‘ 𝑖 ) )
40 37 39 oveq12d ⊢ ( 𝑗 = 𝑖 → ( ( 𝑓 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝑓 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) )
41 38 40 breq12d ⊢ ( 𝑗 = 𝑖 → ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝑓 ‘ 𝑗 ) ) ≤ ( ( 𝑓 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ↔ ( ( 𝐵 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ≤ ( ( 𝑓 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) )
42 41 38 40 ifbieq12d ⊢ ( 𝑗 = 𝑖 → if ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝑓 ‘ 𝑗 ) ) ≤ ( ( 𝑓 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) , ( ( 𝐵 ‘ 𝑗 ) − ( 𝑓 ‘ 𝑗 ) ) , ( ( 𝑓 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ≤ ( ( 𝑓 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) , ( ( 𝑓 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) )
43 42 cbvmptv ⊢ ( 𝑗 ∈ 𝑋 ↦ if ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝑓 ‘ 𝑗 ) ) ≤ ( ( 𝑓 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) , ( ( 𝐵 ‘ 𝑗 ) − ( 𝑓 ‘ 𝑗 ) ) , ( ( 𝑓 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) ) = ( 𝑖 ∈ 𝑋 ↦ if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ≤ ( ( 𝑓 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) , ( ( 𝑓 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) )
44 43 rneqi ⊢ ran ( 𝑗 ∈ 𝑋 ↦ if ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝑓 ‘ 𝑗 ) ) ≤ ( ( 𝑓 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) , ( ( 𝐵 ‘ 𝑗 ) − ( 𝑓 ‘ 𝑗 ) ) , ( ( 𝑓 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) ) = ran ( 𝑖 ∈ 𝑋 ↦ if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ≤ ( ( 𝑓 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) , ( ( 𝑓 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) )
45 44 infeq1i ⊢ inf ( ran ( 𝑗 ∈ 𝑋 ↦ if ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝑓 ‘ 𝑗 ) ) ≤ ( ( 𝑓 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) , ( ( 𝐵 ‘ 𝑗 ) − ( 𝑓 ‘ 𝑗 ) ) , ( ( 𝑓 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) ) , ℝ , < ) = inf ( ran ( 𝑖 ∈ 𝑋 ↦ if ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ≤ ( ( 𝑓 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) , ( ( 𝐵 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) , ( ( 𝑓 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) , ℝ , < )
46 eqid ⊢ ( 𝑓 ( ball ‘ ( 𝑎 ∈ ( ℝ ↑m 𝑋 ) , 𝑏 ∈ ( ℝ ↑m 𝑋 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝑋 ( ( ( 𝑎 ‘ 𝑘 ) − ( 𝑏 ‘ 𝑘 ) ) ↑ 2 ) ) ) ) inf ( ran ( 𝑗 ∈ 𝑋 ↦ if ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝑓 ‘ 𝑗 ) ) ≤ ( ( 𝑓 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) , ( ( 𝐵 ‘ 𝑗 ) − ( 𝑓 ‘ 𝑗 ) ) , ( ( 𝑓 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) ) , ℝ , < ) ) = ( 𝑓 ( ball ‘ ( 𝑎 ∈ ( ℝ ↑m 𝑋 ) , 𝑏 ∈ ( ℝ ↑m 𝑋 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝑋 ( ( ( 𝑎 ‘ 𝑘 ) − ( 𝑏 ‘ 𝑘 ) ) ↑ 2 ) ) ) ) inf ( ran ( 𝑗 ∈ 𝑋 ↦ if ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝑓 ‘ 𝑗 ) ) ≤ ( ( 𝑓 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) , ( ( 𝐵 ‘ 𝑗 ) − ( 𝑓 ‘ 𝑗 ) ) , ( ( 𝑓 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) ) , ℝ , < ) )
47 fveq1 ⊢ ( 𝑎 = 𝑔 → ( 𝑎 ‘ 𝑘 ) = ( 𝑔 ‘ 𝑘 ) )
48 47 oveq1d ⊢ ( 𝑎 = 𝑔 → ( ( 𝑎 ‘ 𝑘 ) − ( 𝑏 ‘ 𝑘 ) ) = ( ( 𝑔 ‘ 𝑘 ) − ( 𝑏 ‘ 𝑘 ) ) )
49 48 oveq1d ⊢ ( 𝑎 = 𝑔 → ( ( ( 𝑎 ‘ 𝑘 ) − ( 𝑏 ‘ 𝑘 ) ) ↑ 2 ) = ( ( ( 𝑔 ‘ 𝑘 ) − ( 𝑏 ‘ 𝑘 ) ) ↑ 2 ) )
50 49 sumeq2sdv ⊢ ( 𝑎 = 𝑔 → Σ 𝑘 ∈ 𝑋 ( ( ( 𝑎 ‘ 𝑘 ) − ( 𝑏 ‘ 𝑘 ) ) ↑ 2 ) = Σ 𝑘 ∈ 𝑋 ( ( ( 𝑔 ‘ 𝑘 ) − ( 𝑏 ‘ 𝑘 ) ) ↑ 2 ) )
51 50 fveq2d ⊢ ( 𝑎 = 𝑔 → ( √ ‘ Σ 𝑘 ∈ 𝑋 ( ( ( 𝑎 ‘ 𝑘 ) − ( 𝑏 ‘ 𝑘 ) ) ↑ 2 ) ) = ( √ ‘ Σ 𝑘 ∈ 𝑋 ( ( ( 𝑔 ‘ 𝑘 ) − ( 𝑏 ‘ 𝑘 ) ) ↑ 2 ) ) )
52 fveq1 ⊢ ( 𝑏 = ℎ → ( 𝑏 ‘ 𝑘 ) = ( ℎ ‘ 𝑘 ) )
53 52 oveq2d ⊢ ( 𝑏 = ℎ → ( ( 𝑔 ‘ 𝑘 ) − ( 𝑏 ‘ 𝑘 ) ) = ( ( 𝑔 ‘ 𝑘 ) − ( ℎ ‘ 𝑘 ) ) )
54 53 oveq1d ⊢ ( 𝑏 = ℎ → ( ( ( 𝑔 ‘ 𝑘 ) − ( 𝑏 ‘ 𝑘 ) ) ↑ 2 ) = ( ( ( 𝑔 ‘ 𝑘 ) − ( ℎ ‘ 𝑘 ) ) ↑ 2 ) )
55 54 sumeq2sdv ⊢ ( 𝑏 = ℎ → Σ 𝑘 ∈ 𝑋 ( ( ( 𝑔 ‘ 𝑘 ) − ( 𝑏 ‘ 𝑘 ) ) ↑ 2 ) = Σ 𝑘 ∈ 𝑋 ( ( ( 𝑔 ‘ 𝑘 ) − ( ℎ ‘ 𝑘 ) ) ↑ 2 ) )
56 55 fveq2d ⊢ ( 𝑏 = ℎ → ( √ ‘ Σ 𝑘 ∈ 𝑋 ( ( ( 𝑔 ‘ 𝑘 ) − ( 𝑏 ‘ 𝑘 ) ) ↑ 2 ) ) = ( √ ‘ Σ 𝑘 ∈ 𝑋 ( ( ( 𝑔 ‘ 𝑘 ) − ( ℎ ‘ 𝑘 ) ) ↑ 2 ) ) )
57 51 56 cbvmpov ⊢ ( 𝑎 ∈ ( ℝ ↑m 𝑋 ) , 𝑏 ∈ ( ℝ ↑m 𝑋 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝑋 ( ( ( 𝑎 ‘ 𝑘 ) − ( 𝑏 ‘ 𝑘 ) ) ↑ 2 ) ) ) = ( 𝑔 ∈ ( ℝ ↑m 𝑋 ) , ℎ ∈ ( ℝ ↑m 𝑋 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝑋 ( ( ( 𝑔 ‘ 𝑘 ) − ( ℎ ‘ 𝑘 ) ) ↑ 2 ) ) )
58 27 29 31 33 34 35 45 46 57 ioorrnopnlem ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐴 ‘ 𝑗 ) (,) ( 𝐵 ‘ 𝑗 ) ) ) → ∃ 𝑣 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ( 𝑓 ∈ 𝑣 ∧ 𝑣 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) )
59 25 58 syldan ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) → ∃ 𝑣 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ( 𝑓 ∈ 𝑣 ∧ 𝑣 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) )
60 59 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ∀ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∃ 𝑣 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ( 𝑓 ∈ 𝑣 ∧ 𝑣 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) )
61 eqid ⊢ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) = ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) )
62 61 rrxtop ⊢ ( 𝑋 ∈ Fin → ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ∈ Top )
63 1 62 syl ⊢ ( 𝜑 → ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ∈ Top )
64 63 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ∈ Top )
65 eltop2 ⊢ ( ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ∈ Top → ( X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ↔ ∀ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∃ 𝑣 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ( 𝑓 ∈ 𝑣 ∧ 𝑣 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) ) )
66 64 65 syl ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ↔ ∀ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∃ 𝑣 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ( 𝑓 ∈ 𝑣 ∧ 𝑣 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) ) )
67 60 66 mpbird ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) )
68 19 67 syldan ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) )
69 17 68 pm2.61dan ⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) )