Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
⊢ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) = ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) |
2 |
1
|
txval |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( 𝑅 ×t 𝑆 ) = ( topGen ‘ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) ) |
3 |
|
bastg |
⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ⊆ ( topGen ‘ 𝑅 ) ) |
4 |
|
bastg |
⊢ ( 𝑆 ∈ 𝑊 → 𝑆 ⊆ ( topGen ‘ 𝑆 ) ) |
5 |
|
resmpo |
⊢ ( ( 𝑅 ⊆ ( topGen ‘ 𝑅 ) ∧ 𝑆 ⊆ ( topGen ‘ 𝑆 ) ) → ( ( 𝑢 ∈ ( topGen ‘ 𝑅 ) , 𝑣 ∈ ( topGen ‘ 𝑆 ) ↦ ( 𝑢 × 𝑣 ) ) ↾ ( 𝑅 × 𝑆 ) ) = ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) |
6 |
3 4 5
|
syl2an |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( ( 𝑢 ∈ ( topGen ‘ 𝑅 ) , 𝑣 ∈ ( topGen ‘ 𝑆 ) ↦ ( 𝑢 × 𝑣 ) ) ↾ ( 𝑅 × 𝑆 ) ) = ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) |
7 |
|
resss |
⊢ ( ( 𝑢 ∈ ( topGen ‘ 𝑅 ) , 𝑣 ∈ ( topGen ‘ 𝑆 ) ↦ ( 𝑢 × 𝑣 ) ) ↾ ( 𝑅 × 𝑆 ) ) ⊆ ( 𝑢 ∈ ( topGen ‘ 𝑅 ) , 𝑣 ∈ ( topGen ‘ 𝑆 ) ↦ ( 𝑢 × 𝑣 ) ) |
8 |
6 7
|
eqsstrrdi |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ⊆ ( 𝑢 ∈ ( topGen ‘ 𝑅 ) , 𝑣 ∈ ( topGen ‘ 𝑆 ) ↦ ( 𝑢 × 𝑣 ) ) ) |
9 |
|
rnss |
⊢ ( ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ⊆ ( 𝑢 ∈ ( topGen ‘ 𝑅 ) , 𝑣 ∈ ( topGen ‘ 𝑆 ) ↦ ( 𝑢 × 𝑣 ) ) → ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ⊆ ran ( 𝑢 ∈ ( topGen ‘ 𝑅 ) , 𝑣 ∈ ( topGen ‘ 𝑆 ) ↦ ( 𝑢 × 𝑣 ) ) ) |
10 |
8 9
|
syl |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ⊆ ran ( 𝑢 ∈ ( topGen ‘ 𝑅 ) , 𝑣 ∈ ( topGen ‘ 𝑆 ) ↦ ( 𝑢 × 𝑣 ) ) ) |
11 |
|
eltg3 |
⊢ ( 𝑅 ∈ 𝑉 → ( 𝑢 ∈ ( topGen ‘ 𝑅 ) ↔ ∃ 𝑚 ( 𝑚 ⊆ 𝑅 ∧ 𝑢 = ∪ 𝑚 ) ) ) |
12 |
|
eltg3 |
⊢ ( 𝑆 ∈ 𝑊 → ( 𝑣 ∈ ( topGen ‘ 𝑆 ) ↔ ∃ 𝑛 ( 𝑛 ⊆ 𝑆 ∧ 𝑣 = ∪ 𝑛 ) ) ) |
13 |
11 12
|
bi2anan9 |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( ( 𝑢 ∈ ( topGen ‘ 𝑅 ) ∧ 𝑣 ∈ ( topGen ‘ 𝑆 ) ) ↔ ( ∃ 𝑚 ( 𝑚 ⊆ 𝑅 ∧ 𝑢 = ∪ 𝑚 ) ∧ ∃ 𝑛 ( 𝑛 ⊆ 𝑆 ∧ 𝑣 = ∪ 𝑛 ) ) ) ) |
14 |
|
exdistrv |
⊢ ( ∃ 𝑚 ∃ 𝑛 ( ( 𝑚 ⊆ 𝑅 ∧ 𝑢 = ∪ 𝑚 ) ∧ ( 𝑛 ⊆ 𝑆 ∧ 𝑣 = ∪ 𝑛 ) ) ↔ ( ∃ 𝑚 ( 𝑚 ⊆ 𝑅 ∧ 𝑢 = ∪ 𝑚 ) ∧ ∃ 𝑛 ( 𝑛 ⊆ 𝑆 ∧ 𝑣 = ∪ 𝑛 ) ) ) |
15 |
|
an4 |
⊢ ( ( ( 𝑚 ⊆ 𝑅 ∧ 𝑢 = ∪ 𝑚 ) ∧ ( 𝑛 ⊆ 𝑆 ∧ 𝑣 = ∪ 𝑛 ) ) ↔ ( ( 𝑚 ⊆ 𝑅 ∧ 𝑛 ⊆ 𝑆 ) ∧ ( 𝑢 = ∪ 𝑚 ∧ 𝑣 = ∪ 𝑛 ) ) ) |
16 |
|
uniiun |
⊢ ∪ 𝑚 = ∪ 𝑥 ∈ 𝑚 𝑥 |
17 |
|
uniiun |
⊢ ∪ 𝑛 = ∪ 𝑦 ∈ 𝑛 𝑦 |
18 |
16 17
|
xpeq12i |
⊢ ( ∪ 𝑚 × ∪ 𝑛 ) = ( ∪ 𝑥 ∈ 𝑚 𝑥 × ∪ 𝑦 ∈ 𝑛 𝑦 ) |
19 |
|
xpiundir |
⊢ ( ∪ 𝑥 ∈ 𝑚 𝑥 × ∪ 𝑦 ∈ 𝑛 𝑦 ) = ∪ 𝑥 ∈ 𝑚 ( 𝑥 × ∪ 𝑦 ∈ 𝑛 𝑦 ) |
20 |
|
xpiundi |
⊢ ( 𝑥 × ∪ 𝑦 ∈ 𝑛 𝑦 ) = ∪ 𝑦 ∈ 𝑛 ( 𝑥 × 𝑦 ) |
21 |
20
|
a1i |
⊢ ( 𝑥 ∈ 𝑚 → ( 𝑥 × ∪ 𝑦 ∈ 𝑛 𝑦 ) = ∪ 𝑦 ∈ 𝑛 ( 𝑥 × 𝑦 ) ) |
22 |
21
|
iuneq2i |
⊢ ∪ 𝑥 ∈ 𝑚 ( 𝑥 × ∪ 𝑦 ∈ 𝑛 𝑦 ) = ∪ 𝑥 ∈ 𝑚 ∪ 𝑦 ∈ 𝑛 ( 𝑥 × 𝑦 ) |
23 |
18 19 22
|
3eqtri |
⊢ ( ∪ 𝑚 × ∪ 𝑛 ) = ∪ 𝑥 ∈ 𝑚 ∪ 𝑦 ∈ 𝑛 ( 𝑥 × 𝑦 ) |
24 |
|
ovex |
⊢ ( 𝑅 ×t 𝑆 ) ∈ V |
25 |
|
ssel2 |
⊢ ( ( 𝑚 ⊆ 𝑅 ∧ 𝑥 ∈ 𝑚 ) → 𝑥 ∈ 𝑅 ) |
26 |
|
ssel2 |
⊢ ( ( 𝑛 ⊆ 𝑆 ∧ 𝑦 ∈ 𝑛 ) → 𝑦 ∈ 𝑆 ) |
27 |
25 26
|
anim12i |
⊢ ( ( ( 𝑚 ⊆ 𝑅 ∧ 𝑥 ∈ 𝑚 ) ∧ ( 𝑛 ⊆ 𝑆 ∧ 𝑦 ∈ 𝑛 ) ) → ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ) |
28 |
27
|
an4s |
⊢ ( ( ( 𝑚 ⊆ 𝑅 ∧ 𝑛 ⊆ 𝑆 ) ∧ ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ) ) → ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ) |
29 |
|
txopn |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 × 𝑦 ) ∈ ( 𝑅 ×t 𝑆 ) ) |
30 |
28 29
|
sylan2 |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( ( 𝑚 ⊆ 𝑅 ∧ 𝑛 ⊆ 𝑆 ) ∧ ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ) ) ) → ( 𝑥 × 𝑦 ) ∈ ( 𝑅 ×t 𝑆 ) ) |
31 |
30
|
anassrs |
⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝑚 ⊆ 𝑅 ∧ 𝑛 ⊆ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ) ) → ( 𝑥 × 𝑦 ) ∈ ( 𝑅 ×t 𝑆 ) ) |
32 |
31
|
anassrs |
⊢ ( ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝑚 ⊆ 𝑅 ∧ 𝑛 ⊆ 𝑆 ) ) ∧ 𝑥 ∈ 𝑚 ) ∧ 𝑦 ∈ 𝑛 ) → ( 𝑥 × 𝑦 ) ∈ ( 𝑅 ×t 𝑆 ) ) |
33 |
32
|
ralrimiva |
⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝑚 ⊆ 𝑅 ∧ 𝑛 ⊆ 𝑆 ) ) ∧ 𝑥 ∈ 𝑚 ) → ∀ 𝑦 ∈ 𝑛 ( 𝑥 × 𝑦 ) ∈ ( 𝑅 ×t 𝑆 ) ) |
34 |
|
tgiun |
⊢ ( ( ( 𝑅 ×t 𝑆 ) ∈ V ∧ ∀ 𝑦 ∈ 𝑛 ( 𝑥 × 𝑦 ) ∈ ( 𝑅 ×t 𝑆 ) ) → ∪ 𝑦 ∈ 𝑛 ( 𝑥 × 𝑦 ) ∈ ( topGen ‘ ( 𝑅 ×t 𝑆 ) ) ) |
35 |
24 33 34
|
sylancr |
⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝑚 ⊆ 𝑅 ∧ 𝑛 ⊆ 𝑆 ) ) ∧ 𝑥 ∈ 𝑚 ) → ∪ 𝑦 ∈ 𝑛 ( 𝑥 × 𝑦 ) ∈ ( topGen ‘ ( 𝑅 ×t 𝑆 ) ) ) |
36 |
1
|
txbasex |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ∈ V ) |
37 |
|
tgidm |
⊢ ( ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ∈ V → ( topGen ‘ ( topGen ‘ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) ) = ( topGen ‘ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) ) |
38 |
36 37
|
syl |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( topGen ‘ ( topGen ‘ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) ) = ( topGen ‘ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) ) |
39 |
2
|
fveq2d |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( topGen ‘ ( 𝑅 ×t 𝑆 ) ) = ( topGen ‘ ( topGen ‘ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) ) ) |
40 |
38 39 2
|
3eqtr4d |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( topGen ‘ ( 𝑅 ×t 𝑆 ) ) = ( 𝑅 ×t 𝑆 ) ) |
41 |
40
|
adantr |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝑚 ⊆ 𝑅 ∧ 𝑛 ⊆ 𝑆 ) ) → ( topGen ‘ ( 𝑅 ×t 𝑆 ) ) = ( 𝑅 ×t 𝑆 ) ) |
42 |
41
|
adantr |
⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝑚 ⊆ 𝑅 ∧ 𝑛 ⊆ 𝑆 ) ) ∧ 𝑥 ∈ 𝑚 ) → ( topGen ‘ ( 𝑅 ×t 𝑆 ) ) = ( 𝑅 ×t 𝑆 ) ) |
43 |
35 42
|
eleqtrd |
⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝑚 ⊆ 𝑅 ∧ 𝑛 ⊆ 𝑆 ) ) ∧ 𝑥 ∈ 𝑚 ) → ∪ 𝑦 ∈ 𝑛 ( 𝑥 × 𝑦 ) ∈ ( 𝑅 ×t 𝑆 ) ) |
44 |
43
|
ralrimiva |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝑚 ⊆ 𝑅 ∧ 𝑛 ⊆ 𝑆 ) ) → ∀ 𝑥 ∈ 𝑚 ∪ 𝑦 ∈ 𝑛 ( 𝑥 × 𝑦 ) ∈ ( 𝑅 ×t 𝑆 ) ) |
45 |
|
tgiun |
⊢ ( ( ( 𝑅 ×t 𝑆 ) ∈ V ∧ ∀ 𝑥 ∈ 𝑚 ∪ 𝑦 ∈ 𝑛 ( 𝑥 × 𝑦 ) ∈ ( 𝑅 ×t 𝑆 ) ) → ∪ 𝑥 ∈ 𝑚 ∪ 𝑦 ∈ 𝑛 ( 𝑥 × 𝑦 ) ∈ ( topGen ‘ ( 𝑅 ×t 𝑆 ) ) ) |
46 |
24 44 45
|
sylancr |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝑚 ⊆ 𝑅 ∧ 𝑛 ⊆ 𝑆 ) ) → ∪ 𝑥 ∈ 𝑚 ∪ 𝑦 ∈ 𝑛 ( 𝑥 × 𝑦 ) ∈ ( topGen ‘ ( 𝑅 ×t 𝑆 ) ) ) |
47 |
46 41
|
eleqtrd |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝑚 ⊆ 𝑅 ∧ 𝑛 ⊆ 𝑆 ) ) → ∪ 𝑥 ∈ 𝑚 ∪ 𝑦 ∈ 𝑛 ( 𝑥 × 𝑦 ) ∈ ( 𝑅 ×t 𝑆 ) ) |
48 |
23 47
|
eqeltrid |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝑚 ⊆ 𝑅 ∧ 𝑛 ⊆ 𝑆 ) ) → ( ∪ 𝑚 × ∪ 𝑛 ) ∈ ( 𝑅 ×t 𝑆 ) ) |
49 |
|
xpeq12 |
⊢ ( ( 𝑢 = ∪ 𝑚 ∧ 𝑣 = ∪ 𝑛 ) → ( 𝑢 × 𝑣 ) = ( ∪ 𝑚 × ∪ 𝑛 ) ) |
50 |
49
|
eleq1d |
⊢ ( ( 𝑢 = ∪ 𝑚 ∧ 𝑣 = ∪ 𝑛 ) → ( ( 𝑢 × 𝑣 ) ∈ ( 𝑅 ×t 𝑆 ) ↔ ( ∪ 𝑚 × ∪ 𝑛 ) ∈ ( 𝑅 ×t 𝑆 ) ) ) |
51 |
48 50
|
syl5ibrcom |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝑚 ⊆ 𝑅 ∧ 𝑛 ⊆ 𝑆 ) ) → ( ( 𝑢 = ∪ 𝑚 ∧ 𝑣 = ∪ 𝑛 ) → ( 𝑢 × 𝑣 ) ∈ ( 𝑅 ×t 𝑆 ) ) ) |
52 |
51
|
expimpd |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( ( ( 𝑚 ⊆ 𝑅 ∧ 𝑛 ⊆ 𝑆 ) ∧ ( 𝑢 = ∪ 𝑚 ∧ 𝑣 = ∪ 𝑛 ) ) → ( 𝑢 × 𝑣 ) ∈ ( 𝑅 ×t 𝑆 ) ) ) |
53 |
15 52
|
syl5bi |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( ( ( 𝑚 ⊆ 𝑅 ∧ 𝑢 = ∪ 𝑚 ) ∧ ( 𝑛 ⊆ 𝑆 ∧ 𝑣 = ∪ 𝑛 ) ) → ( 𝑢 × 𝑣 ) ∈ ( 𝑅 ×t 𝑆 ) ) ) |
54 |
53
|
exlimdvv |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( ∃ 𝑚 ∃ 𝑛 ( ( 𝑚 ⊆ 𝑅 ∧ 𝑢 = ∪ 𝑚 ) ∧ ( 𝑛 ⊆ 𝑆 ∧ 𝑣 = ∪ 𝑛 ) ) → ( 𝑢 × 𝑣 ) ∈ ( 𝑅 ×t 𝑆 ) ) ) |
55 |
14 54
|
syl5bir |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( ( ∃ 𝑚 ( 𝑚 ⊆ 𝑅 ∧ 𝑢 = ∪ 𝑚 ) ∧ ∃ 𝑛 ( 𝑛 ⊆ 𝑆 ∧ 𝑣 = ∪ 𝑛 ) ) → ( 𝑢 × 𝑣 ) ∈ ( 𝑅 ×t 𝑆 ) ) ) |
56 |
13 55
|
sylbid |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( ( 𝑢 ∈ ( topGen ‘ 𝑅 ) ∧ 𝑣 ∈ ( topGen ‘ 𝑆 ) ) → ( 𝑢 × 𝑣 ) ∈ ( 𝑅 ×t 𝑆 ) ) ) |
57 |
56
|
ralrimivv |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ∀ 𝑢 ∈ ( topGen ‘ 𝑅 ) ∀ 𝑣 ∈ ( topGen ‘ 𝑆 ) ( 𝑢 × 𝑣 ) ∈ ( 𝑅 ×t 𝑆 ) ) |
58 |
|
eqid |
⊢ ( 𝑢 ∈ ( topGen ‘ 𝑅 ) , 𝑣 ∈ ( topGen ‘ 𝑆 ) ↦ ( 𝑢 × 𝑣 ) ) = ( 𝑢 ∈ ( topGen ‘ 𝑅 ) , 𝑣 ∈ ( topGen ‘ 𝑆 ) ↦ ( 𝑢 × 𝑣 ) ) |
59 |
58
|
fmpo |
⊢ ( ∀ 𝑢 ∈ ( topGen ‘ 𝑅 ) ∀ 𝑣 ∈ ( topGen ‘ 𝑆 ) ( 𝑢 × 𝑣 ) ∈ ( 𝑅 ×t 𝑆 ) ↔ ( 𝑢 ∈ ( topGen ‘ 𝑅 ) , 𝑣 ∈ ( topGen ‘ 𝑆 ) ↦ ( 𝑢 × 𝑣 ) ) : ( ( topGen ‘ 𝑅 ) × ( topGen ‘ 𝑆 ) ) ⟶ ( 𝑅 ×t 𝑆 ) ) |
60 |
57 59
|
sylib |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( 𝑢 ∈ ( topGen ‘ 𝑅 ) , 𝑣 ∈ ( topGen ‘ 𝑆 ) ↦ ( 𝑢 × 𝑣 ) ) : ( ( topGen ‘ 𝑅 ) × ( topGen ‘ 𝑆 ) ) ⟶ ( 𝑅 ×t 𝑆 ) ) |
61 |
60
|
frnd |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ran ( 𝑢 ∈ ( topGen ‘ 𝑅 ) , 𝑣 ∈ ( topGen ‘ 𝑆 ) ↦ ( 𝑢 × 𝑣 ) ) ⊆ ( 𝑅 ×t 𝑆 ) ) |
62 |
61 2
|
sseqtrd |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ran ( 𝑢 ∈ ( topGen ‘ 𝑅 ) , 𝑣 ∈ ( topGen ‘ 𝑆 ) ↦ ( 𝑢 × 𝑣 ) ) ⊆ ( topGen ‘ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) ) |
63 |
|
2basgen |
⊢ ( ( ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ⊆ ran ( 𝑢 ∈ ( topGen ‘ 𝑅 ) , 𝑣 ∈ ( topGen ‘ 𝑆 ) ↦ ( 𝑢 × 𝑣 ) ) ∧ ran ( 𝑢 ∈ ( topGen ‘ 𝑅 ) , 𝑣 ∈ ( topGen ‘ 𝑆 ) ↦ ( 𝑢 × 𝑣 ) ) ⊆ ( topGen ‘ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) ) → ( topGen ‘ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) = ( topGen ‘ ran ( 𝑢 ∈ ( topGen ‘ 𝑅 ) , 𝑣 ∈ ( topGen ‘ 𝑆 ) ↦ ( 𝑢 × 𝑣 ) ) ) ) |
64 |
10 62 63
|
syl2anc |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( topGen ‘ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) = ( topGen ‘ ran ( 𝑢 ∈ ( topGen ‘ 𝑅 ) , 𝑣 ∈ ( topGen ‘ 𝑆 ) ↦ ( 𝑢 × 𝑣 ) ) ) ) |
65 |
|
fvex |
⊢ ( topGen ‘ 𝑅 ) ∈ V |
66 |
|
fvex |
⊢ ( topGen ‘ 𝑆 ) ∈ V |
67 |
|
eqid |
⊢ ran ( 𝑢 ∈ ( topGen ‘ 𝑅 ) , 𝑣 ∈ ( topGen ‘ 𝑆 ) ↦ ( 𝑢 × 𝑣 ) ) = ran ( 𝑢 ∈ ( topGen ‘ 𝑅 ) , 𝑣 ∈ ( topGen ‘ 𝑆 ) ↦ ( 𝑢 × 𝑣 ) ) |
68 |
67
|
txval |
⊢ ( ( ( topGen ‘ 𝑅 ) ∈ V ∧ ( topGen ‘ 𝑆 ) ∈ V ) → ( ( topGen ‘ 𝑅 ) ×t ( topGen ‘ 𝑆 ) ) = ( topGen ‘ ran ( 𝑢 ∈ ( topGen ‘ 𝑅 ) , 𝑣 ∈ ( topGen ‘ 𝑆 ) ↦ ( 𝑢 × 𝑣 ) ) ) ) |
69 |
65 66 68
|
mp2an |
⊢ ( ( topGen ‘ 𝑅 ) ×t ( topGen ‘ 𝑆 ) ) = ( topGen ‘ ran ( 𝑢 ∈ ( topGen ‘ 𝑅 ) , 𝑣 ∈ ( topGen ‘ 𝑆 ) ↦ ( 𝑢 × 𝑣 ) ) ) |
70 |
64 69
|
eqtr4di |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( topGen ‘ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) = ( ( topGen ‘ 𝑅 ) ×t ( topGen ‘ 𝑆 ) ) ) |
71 |
2 70
|
eqtr2d |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( ( topGen ‘ 𝑅 ) ×t ( topGen ‘ 𝑆 ) ) = ( 𝑅 ×t 𝑆 ) ) |