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 )