Metamath Proof Explorer

Theorem ioorrnopnxr

Description: The indexed product of open intervals is an open set in ( RR^X ) . Similar to ioorrnopn but here unbounded intervals are allowed. (Contributed by Glauco Siliprandi, 8-Apr-2021)

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

Proof

Step Hyp Ref Expression
1 ioorrnopnxr.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
2 ioorrnopnxr.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ* )
3 ioorrnopnxr.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 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐴 ‘ 𝑗 ) (,) ( 𝐵 ‘ 𝑗 ) ) ) → 𝐴 : 𝑋 ⟶ ℝ* )
28 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐴 ‘ 𝑗 ) (,) ( 𝐵 ‘ 𝑗 ) ) ) → 𝐵 : 𝑋 ⟶ ℝ* )
29 24 bilanri ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐴 ‘ 𝑗 ) (,) ( 𝐵 ‘ 𝑗 ) ) ) → 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) )
30 fveq2 ⊢ ( 𝑗 = 𝑖 → ( 𝐴 ‘ 𝑗 ) = ( 𝐴 ‘ 𝑖 ) )
31 30 eqeq1d ⊢ ( 𝑗 = 𝑖 → ( ( 𝐴 ‘ 𝑗 ) = -∞ ↔ ( 𝐴 ‘ 𝑖 ) = -∞ ) )
32 fveq2 ⊢ ( 𝑗 = 𝑖 → ( 𝑓 ‘ 𝑗 ) = ( 𝑓 ‘ 𝑖 ) )
33 32 oveq1d ⊢ ( 𝑗 = 𝑖 → ( ( 𝑓 ‘ 𝑗 ) − 1 ) = ( ( 𝑓 ‘ 𝑖 ) − 1 ) )
34 31 33 30 ifbieq12d ⊢ ( 𝑗 = 𝑖 → if ( ( 𝐴 ‘ 𝑗 ) = -∞ , ( ( 𝑓 ‘ 𝑗 ) − 1 ) , ( 𝐴 ‘ 𝑗 ) ) = if ( ( 𝐴 ‘ 𝑖 ) = -∞ , ( ( 𝑓 ‘ 𝑖 ) − 1 ) , ( 𝐴 ‘ 𝑖 ) ) )
35 34 cbvmptv ⊢ ( 𝑗 ∈ 𝑋 ↦ if ( ( 𝐴 ‘ 𝑗 ) = -∞ , ( ( 𝑓 ‘ 𝑗 ) − 1 ) , ( 𝐴 ‘ 𝑗 ) ) ) = ( 𝑖 ∈ 𝑋 ↦ if ( ( 𝐴 ‘ 𝑖 ) = -∞ , ( ( 𝑓 ‘ 𝑖 ) − 1 ) , ( 𝐴 ‘ 𝑖 ) ) )
36 fveq2 ⊢ ( 𝑗 = 𝑖 → ( 𝐵 ‘ 𝑗 ) = ( 𝐵 ‘ 𝑖 ) )
37 36 eqeq1d ⊢ ( 𝑗 = 𝑖 → ( ( 𝐵 ‘ 𝑗 ) = +∞ ↔ ( 𝐵 ‘ 𝑖 ) = +∞ ) )
38 32 oveq1d ⊢ ( 𝑗 = 𝑖 → ( ( 𝑓 ‘ 𝑗 ) + 1 ) = ( ( 𝑓 ‘ 𝑖 ) + 1 ) )
39 37 38 36 ifbieq12d ⊢ ( 𝑗 = 𝑖 → if ( ( 𝐵 ‘ 𝑗 ) = +∞ , ( ( 𝑓 ‘ 𝑗 ) + 1 ) , ( 𝐵 ‘ 𝑗 ) ) = if ( ( 𝐵 ‘ 𝑖 ) = +∞ , ( ( 𝑓 ‘ 𝑖 ) + 1 ) , ( 𝐵 ‘ 𝑖 ) ) )
40 39 cbvmptv ⊢ ( 𝑗 ∈ 𝑋 ↦ if ( ( 𝐵 ‘ 𝑗 ) = +∞ , ( ( 𝑓 ‘ 𝑗 ) + 1 ) , ( 𝐵 ‘ 𝑗 ) ) ) = ( 𝑖 ∈ 𝑋 ↦ if ( ( 𝐵 ‘ 𝑖 ) = +∞ , ( ( 𝑓 ‘ 𝑖 ) + 1 ) , ( 𝐵 ‘ 𝑖 ) ) )
41 eqid ⊢ X 𝑖 ∈ 𝑋 ( ( ( 𝑗 ∈ 𝑋 ↦ if ( ( 𝐴 ‘ 𝑗 ) = -∞ , ( ( 𝑓 ‘ 𝑗 ) − 1 ) , ( 𝐴 ‘ 𝑗 ) ) ) ‘ 𝑖 ) (,) ( ( 𝑗 ∈ 𝑋 ↦ if ( ( 𝐵 ‘ 𝑗 ) = +∞ , ( ( 𝑓 ‘ 𝑗 ) + 1 ) , ( 𝐵 ‘ 𝑗 ) ) ) ‘ 𝑖 ) ) = X 𝑖 ∈ 𝑋 ( ( ( 𝑗 ∈ 𝑋 ↦ if ( ( 𝐴 ‘ 𝑗 ) = -∞ , ( ( 𝑓 ‘ 𝑗 ) − 1 ) , ( 𝐴 ‘ 𝑗 ) ) ) ‘ 𝑖 ) (,) ( ( 𝑗 ∈ 𝑋 ↦ if ( ( 𝐵 ‘ 𝑗 ) = +∞ , ( ( 𝑓 ‘ 𝑗 ) + 1 ) , ( 𝐵 ‘ 𝑗 ) ) ) ‘ 𝑖 ) )
42 26 27 28 29 35 40 41 ioorrnopnxrlem ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐴 ‘ 𝑗 ) (,) ( 𝐵 ‘ 𝑗 ) ) ) → ∃ 𝑣 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ( 𝑓 ∈ 𝑣 ∧ 𝑣 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) )
43 25 42 syldan ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) → ∃ 𝑣 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ( 𝑓 ∈ 𝑣 ∧ 𝑣 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) )
44 43 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ∀ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∃ 𝑣 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ( 𝑓 ∈ 𝑣 ∧ 𝑣 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) )
45 eqid ⊢ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) = ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) )
46 45 rrxtop ⊢ ( 𝑋 ∈ Fin → ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ∈ Top )
47 1 46 syl ⊢ ( 𝜑 → ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ∈ Top )
48 47 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ∈ Top )
49 eltop2 ⊢ ( ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ∈ Top → ( X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ↔ ∀ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∃ 𝑣 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ( 𝑓 ∈ 𝑣 ∧ 𝑣 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) ) )
50 48 49 syl ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ↔ ∀ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∃ 𝑣 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ( 𝑓 ∈ 𝑣 ∧ 𝑣 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) ) )
51 44 50 mpbird ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) )
52 19 51 syldan ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) )
53 17 52 pm2.61dan ⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) )