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