Theorem txval

Description: Value of the binary topological product operation. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 30-Aug-2015)

	Ref	Expression
Hypothesis	txval.1	⊢ 𝐵 = ran ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) )
Assertion	txval	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( 𝑅 ×t 𝑆 ) = ( topGen ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		txval.1	⊢ 𝐵 = ran ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) )
2		elex	⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V )
3		elex	⊢ ( 𝑆 ∈ 𝑊 → 𝑆 ∈ V )
4		mpoeq12	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) = ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) ) )
5	4	rneqd	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ran ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) = ran ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) ) )
6	5 1	eqtr4di	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ran ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) = 𝐵 )
7	6	fveq2d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( topGen ‘ ran ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) ) = ( topGen ‘ 𝐵 ) )
8		df-tx	⊢ ×t = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ ( topGen ‘ ran ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) ) )
9		fvex	⊢ ( topGen ‘ 𝐵 ) ∈ V
10	7 8 9	ovmpoa	⊢ ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) → ( 𝑅 ×t 𝑆 ) = ( topGen ‘ 𝐵 ) )
11	2 3 10	syl2an	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( 𝑅 ×t 𝑆 ) = ( topGen ‘ 𝐵 ) )