Step |
Hyp |
Ref |
Expression |
1 |
|
topontop |
⊢ ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) → 𝑅 ∈ Top ) |
2 |
|
topontop |
⊢ ( 𝑆 ∈ ( TopOn ‘ 𝑌 ) → 𝑆 ∈ Top ) |
3 |
|
txtop |
⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 ×t 𝑆 ) ∈ Top ) |
4 |
1 2 3
|
syl2an |
⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑅 ×t 𝑆 ) ∈ Top ) |
5 |
|
eqid |
⊢ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) = ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) |
6 |
|
eqid |
⊢ ∪ 𝑅 = ∪ 𝑅 |
7 |
|
eqid |
⊢ ∪ 𝑆 = ∪ 𝑆 |
8 |
5 6 7
|
txuni2 |
⊢ ( ∪ 𝑅 × ∪ 𝑆 ) = ∪ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) |
9 |
|
toponuni |
⊢ ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝑅 ) |
10 |
|
toponuni |
⊢ ( 𝑆 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 = ∪ 𝑆 ) |
11 |
|
xpeq12 |
⊢ ( ( 𝑋 = ∪ 𝑅 ∧ 𝑌 = ∪ 𝑆 ) → ( 𝑋 × 𝑌 ) = ( ∪ 𝑅 × ∪ 𝑆 ) ) |
12 |
9 10 11
|
syl2an |
⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑋 × 𝑌 ) = ( ∪ 𝑅 × ∪ 𝑆 ) ) |
13 |
5
|
txbasex |
⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ∈ V ) |
14 |
|
unitg |
⊢ ( ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ∈ V → ∪ ( topGen ‘ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) = ∪ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) |
15 |
13 14
|
syl |
⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ∪ ( topGen ‘ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) = ∪ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) |
16 |
8 12 15
|
3eqtr4a |
⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑋 × 𝑌 ) = ∪ ( topGen ‘ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) ) |
17 |
5
|
txval |
⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑅 ×t 𝑆 ) = ( topGen ‘ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) ) |
18 |
17
|
unieqd |
⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ∪ ( 𝑅 ×t 𝑆 ) = ∪ ( topGen ‘ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) ) |
19 |
16 18
|
eqtr4d |
⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑋 × 𝑌 ) = ∪ ( 𝑅 ×t 𝑆 ) ) |
20 |
|
istopon |
⊢ ( ( 𝑅 ×t 𝑆 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ↔ ( ( 𝑅 ×t 𝑆 ) ∈ Top ∧ ( 𝑋 × 𝑌 ) = ∪ ( 𝑅 ×t 𝑆 ) ) ) |
21 |
4 19 20
|
sylanbrc |
⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑅 ×t 𝑆 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ) |