Metamath Proof Explorer

Theorem elsx

Description: The cartesian product of two open sets is an element of the product sigma-algebra. (Contributed by Thierry Arnoux, 3-Jun-2017)

Ref Expression
Assertion elsx ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → ( 𝐴 × 𝐵 ) ∈ ( 𝑆 ×s 𝑇 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) = ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) )
2 1 txbasex ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊 ) → ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ∈ V )
3 sssigagen ⊢ ( ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ∈ V → ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ⊆ ( sigaGen ‘ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ) )
4 2 3 syl ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊 ) → ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ⊆ ( sigaGen ‘ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ) )
5 4 adantr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ⊆ ( sigaGen ‘ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ) )
6 eqid ⊢ ( 𝐴 × 𝐵 ) = ( 𝐴 × 𝐵 )
7 xpeq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 × 𝑦 ) = ( 𝐴 × 𝑦 ) )
8 7 eqeq2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐴 × 𝐵 ) = ( 𝑥 × 𝑦 ) ↔ ( 𝐴 × 𝐵 ) = ( 𝐴 × 𝑦 ) ) )
9 xpeq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 × 𝑦 ) = ( 𝐴 × 𝐵 ) )
10 9 eqeq2d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 × 𝐵 ) = ( 𝐴 × 𝑦 ) ↔ ( 𝐴 × 𝐵 ) = ( 𝐴 × 𝐵 ) ) )
11 8 10 rspc2ev ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ∧ ( 𝐴 × 𝐵 ) = ( 𝐴 × 𝐵 ) ) → ∃ 𝑥 ∈ 𝑆 ∃ 𝑦 ∈ 𝑇 ( 𝐴 × 𝐵 ) = ( 𝑥 × 𝑦 ) )
12 6 11 mp3an3 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) → ∃ 𝑥 ∈ 𝑆 ∃ 𝑦 ∈ 𝑇 ( 𝐴 × 𝐵 ) = ( 𝑥 × 𝑦 ) )
13 xpexg ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) → ( 𝐴 × 𝐵 ) ∈ V )
14 eqid ⊢ ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) )
15 14 elrnmpog ⊢ ( ( 𝐴 × 𝐵 ) ∈ V → ( ( 𝐴 × 𝐵 ) ∈ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ↔ ∃ 𝑥 ∈ 𝑆 ∃ 𝑦 ∈ 𝑇 ( 𝐴 × 𝐵 ) = ( 𝑥 × 𝑦 ) ) )
16 13 15 syl ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) → ( ( 𝐴 × 𝐵 ) ∈ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ↔ ∃ 𝑥 ∈ 𝑆 ∃ 𝑦 ∈ 𝑇 ( 𝐴 × 𝐵 ) = ( 𝑥 × 𝑦 ) ) )
17 12 16 mpbird ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) → ( 𝐴 × 𝐵 ) ∈ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) )
18 17 adantl ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → ( 𝐴 × 𝐵 ) ∈ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) )
19 5 18 sseldd ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → ( 𝐴 × 𝐵 ) ∈ ( sigaGen ‘ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ) )
20 1 sxval ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊 ) → ( 𝑆 ×s 𝑇 ) = ( sigaGen ‘ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ) )
21 20 adantr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → ( 𝑆 ×s 𝑇 ) = ( sigaGen ‘ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ) )
22 19 21 eleqtrrd ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → ( 𝐴 × 𝐵 ) ∈ ( 𝑆 ×s 𝑇 ) )