This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xpstps

Description: A binary product of topologies is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015)

Ref Expression
Hypothesis xpstps.t ⊢ 𝑇 = ( 𝑅 ×s 𝑆 )
Assertion xpstps ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → 𝑇 ∈ TopSp )

Proof

Step Hyp Ref Expression
1 xpstps.t ⊢ 𝑇 = ( 𝑅 ×s 𝑆 )
2 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
3 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
4 simpl ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → 𝑅 ∈ TopSp )
5 simpr ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → 𝑆 ∈ TopSp )
6 eqid ⊢ ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) = ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
7 eqid ⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
8 eqid ⊢ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) = ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } )
9 1 2 3 4 5 6 7 8 xpsval ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → 𝑇 = ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) “s ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
10 1 2 3 4 5 6 7 8 xpsrnbas ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
11 6 xpsff1o2 ⊢ ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑆 ) ) –1-1-onto→ ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
12 11 a1i ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑆 ) ) –1-1-onto→ ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) )
13 f1ocnv ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑆 ) ) –1-1-onto→ ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) → ◡ ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –1-1-onto→ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑆 ) ) )
14 f1ofo ⊢ ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –1-1-onto→ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑆 ) ) → ◡ ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –onto→ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑆 ) ) )
15 12 13 14 3syl ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ◡ ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –onto→ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑆 ) ) )
16 fvexd ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( Scalar ‘ 𝑅 ) ∈ V )
17 2on ⊢ 2o ∈ On
18 17 a1i ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → 2o ∈ On )
19 xpscf ⊢ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } : 2o ⟶ TopSp ↔ ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) )
20 19 biimpri ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } : 2o ⟶ TopSp )
21 8 16 18 20 prdstps ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ∈ TopSp )
22 9 10 15 21 imastps ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → 𝑇 ∈ TopSp )