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