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

Metamath Proof Explorer

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 ‘ 𝐵 ) )