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