Metamath Proof Explorer

Theorem txbasval

Description: It is sufficient to consider products of the bases for the topologies in the topological product. (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Assertion txbasval ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( ( topGen ‘ 𝑅 ) ×t ( topGen ‘ 𝑆 ) ) = ( 𝑅 ×t 𝑆 ) )

Proof

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 𝑆 ) )