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