Metamath Proof Explorer

Theorem tx2ndc

Description: The topological product of two second-countable spaces is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion tx2ndc ( ( 𝑅 ∈ 2ndω ∧ 𝑆 ∈ 2ndω ) → ( 𝑅 ×t 𝑆 ) ∈ 2ndω )

Proof

Step Hyp Ref Expression
1 is2ndc ⊢ ( 𝑅 ∈ 2ndω ↔ ∃ 𝑟 ∈ TopBases ( 𝑟 ≼ ω ∧ ( topGen ‘ 𝑟 ) = 𝑅 ) )
2 is2ndc ⊢ ( 𝑆 ∈ 2ndω ↔ ∃ 𝑠 ∈ TopBases ( 𝑠 ≼ ω ∧ ( topGen ‘ 𝑠 ) = 𝑆 ) )
3 reeanv ⊢ ( ∃ 𝑟 ∈ TopBases ∃ 𝑠 ∈ TopBases ( ( 𝑟 ≼ ω ∧ ( topGen ‘ 𝑟 ) = 𝑅 ) ∧ ( 𝑠 ≼ ω ∧ ( topGen ‘ 𝑠 ) = 𝑆 ) ) ↔ ( ∃ 𝑟 ∈ TopBases ( 𝑟 ≼ ω ∧ ( topGen ‘ 𝑟 ) = 𝑅 ) ∧ ∃ 𝑠 ∈ TopBases ( 𝑠 ≼ ω ∧ ( topGen ‘ 𝑠 ) = 𝑆 ) ) )
4 an4 ⊢ ( ( ( 𝑟 ≼ ω ∧ ( topGen ‘ 𝑟 ) = 𝑅 ) ∧ ( 𝑠 ≼ ω ∧ ( topGen ‘ 𝑠 ) = 𝑆 ) ) ↔ ( ( 𝑟 ≼ ω ∧ 𝑠 ≼ ω ) ∧ ( ( topGen ‘ 𝑟 ) = 𝑅 ∧ ( topGen ‘ 𝑠 ) = 𝑆 ) ) )
5 txbasval ⊢ ( ( 𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases ) → ( ( topGen ‘ 𝑟 ) ×t ( topGen ‘ 𝑠 ) ) = ( 𝑟 ×t 𝑠 ) )
6 eqid ⊢ ran ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) = ran ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) )
7 6 txval ⊢ ( ( 𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases ) → ( 𝑟 ×t 𝑠 ) = ( topGen ‘ ran ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) ) )
8 5 7 eqtrd ⊢ ( ( 𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases ) → ( ( topGen ‘ 𝑟 ) ×t ( topGen ‘ 𝑠 ) ) = ( topGen ‘ ran ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) ) )
9 8 adantr ⊢ ( ( ( 𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases ) ∧ ( 𝑟 ≼ ω ∧ 𝑠 ≼ ω ) ) → ( ( topGen ‘ 𝑟 ) ×t ( topGen ‘ 𝑠 ) ) = ( topGen ‘ ran ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) ) )
10 6 txbas ⊢ ( ( 𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases ) → ran ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) ∈ TopBases )
11 10 adantr ⊢ ( ( ( 𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases ) ∧ ( 𝑟 ≼ ω ∧ 𝑠 ≼ ω ) ) → ran ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) ∈ TopBases )
12 omelon ⊢ ω ∈ On
13 vex ⊢ 𝑠 ∈ V
14 13 xpdom1 ⊢ ( 𝑟 ≼ ω → ( 𝑟 × 𝑠 ) ≼ ( ω × 𝑠 ) )
15 omex ⊢ ω ∈ V
16 15 xpdom2 ⊢ ( 𝑠 ≼ ω → ( ω × 𝑠 ) ≼ ( ω × ω ) )
17 domtr ⊢ ( ( ( 𝑟 × 𝑠 ) ≼ ( ω × 𝑠 ) ∧ ( ω × 𝑠 ) ≼ ( ω × ω ) ) → ( 𝑟 × 𝑠 ) ≼ ( ω × ω ) )
18 14 16 17 syl2an ⊢ ( ( 𝑟 ≼ ω ∧ 𝑠 ≼ ω ) → ( 𝑟 × 𝑠 ) ≼ ( ω × ω ) )
19 18 adantl ⊢ ( ( ( 𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases ) ∧ ( 𝑟 ≼ ω ∧ 𝑠 ≼ ω ) ) → ( 𝑟 × 𝑠 ) ≼ ( ω × ω ) )
20 xpomen ⊢ ( ω × ω ) ≈ ω
21 domentr ⊢ ( ( ( 𝑟 × 𝑠 ) ≼ ( ω × ω ) ∧ ( ω × ω ) ≈ ω ) → ( 𝑟 × 𝑠 ) ≼ ω )
22 19 20 21 sylancl ⊢ ( ( ( 𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases ) ∧ ( 𝑟 ≼ ω ∧ 𝑠 ≼ ω ) ) → ( 𝑟 × 𝑠 ) ≼ ω )
23 ondomen ⊢ ( ( ω ∈ On ∧ ( 𝑟 × 𝑠 ) ≼ ω ) → ( 𝑟 × 𝑠 ) ∈ dom card )
24 12 22 23 sylancr ⊢ ( ( ( 𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases ) ∧ ( 𝑟 ≼ ω ∧ 𝑠 ≼ ω ) ) → ( 𝑟 × 𝑠 ) ∈ dom card )
25 eqid ⊢ ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) = ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) )
26 vex ⊢ 𝑥 ∈ V
27 vex ⊢ 𝑦 ∈ V
28 26 27 xpex ⊢ ( 𝑥 × 𝑦 ) ∈ V
29 25 28 fnmpoi ⊢ ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) Fn ( 𝑟 × 𝑠 )
30 29 a1i ⊢ ( ( ( 𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases ) ∧ ( 𝑟 ≼ ω ∧ 𝑠 ≼ ω ) ) → ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) Fn ( 𝑟 × 𝑠 ) )
31 dffn4 ⊢ ( ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) Fn ( 𝑟 × 𝑠 ) ↔ ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) : ( 𝑟 × 𝑠 ) –onto→ ran ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) )
32 30 31 sylib ⊢ ( ( ( 𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases ) ∧ ( 𝑟 ≼ ω ∧ 𝑠 ≼ ω ) ) → ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) : ( 𝑟 × 𝑠 ) –onto→ ran ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) )
33 fodomnum ⊢ ( ( 𝑟 × 𝑠 ) ∈ dom card → ( ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) : ( 𝑟 × 𝑠 ) –onto→ ran ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) → ran ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) ≼ ( 𝑟 × 𝑠 ) ) )
34 24 32 33 sylc ⊢ ( ( ( 𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases ) ∧ ( 𝑟 ≼ ω ∧ 𝑠 ≼ ω ) ) → ran ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) ≼ ( 𝑟 × 𝑠 ) )
35 domtr ⊢ ( ( ran ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) ≼ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ≼ ω ) → ran ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) ≼ ω )
36 34 22 35 syl2anc ⊢ ( ( ( 𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases ) ∧ ( 𝑟 ≼ ω ∧ 𝑠 ≼ ω ) ) → ran ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) ≼ ω )
37 2ndci ⊢ ( ( ran ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) ∈ TopBases ∧ ran ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) ≼ ω ) → ( topGen ‘ ran ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) ) ∈ 2ndω )
38 11 36 37 syl2anc ⊢ ( ( ( 𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases ) ∧ ( 𝑟 ≼ ω ∧ 𝑠 ≼ ω ) ) → ( topGen ‘ ran ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) ) ∈ 2ndω )
39 9 38 eqeltrd ⊢ ( ( ( 𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases ) ∧ ( 𝑟 ≼ ω ∧ 𝑠 ≼ ω ) ) → ( ( topGen ‘ 𝑟 ) ×t ( topGen ‘ 𝑠 ) ) ∈ 2ndω )
40 oveq12 ⊢ ( ( ( topGen ‘ 𝑟 ) = 𝑅 ∧ ( topGen ‘ 𝑠 ) = 𝑆 ) → ( ( topGen ‘ 𝑟 ) ×t ( topGen ‘ 𝑠 ) ) = ( 𝑅 ×t 𝑆 ) )
41 40 eleq1d ⊢ ( ( ( topGen ‘ 𝑟 ) = 𝑅 ∧ ( topGen ‘ 𝑠 ) = 𝑆 ) → ( ( ( topGen ‘ 𝑟 ) ×t ( topGen ‘ 𝑠 ) ) ∈ 2ndω ↔ ( 𝑅 ×t 𝑆 ) ∈ 2ndω ) )
42 39 41 syl5ibcom ⊢ ( ( ( 𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases ) ∧ ( 𝑟 ≼ ω ∧ 𝑠 ≼ ω ) ) → ( ( ( topGen ‘ 𝑟 ) = 𝑅 ∧ ( topGen ‘ 𝑠 ) = 𝑆 ) → ( 𝑅 ×t 𝑆 ) ∈ 2ndω ) )
43 42 expimpd ⊢ ( ( 𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases ) → ( ( ( 𝑟 ≼ ω ∧ 𝑠 ≼ ω ) ∧ ( ( topGen ‘ 𝑟 ) = 𝑅 ∧ ( topGen ‘ 𝑠 ) = 𝑆 ) ) → ( 𝑅 ×t 𝑆 ) ∈ 2ndω ) )
44 4 43 syl5bi ⊢ ( ( 𝑟 ∈ TopBases ∧ 𝑠 ∈ TopBases ) → ( ( ( 𝑟 ≼ ω ∧ ( topGen ‘ 𝑟 ) = 𝑅 ) ∧ ( 𝑠 ≼ ω ∧ ( topGen ‘ 𝑠 ) = 𝑆 ) ) → ( 𝑅 ×t 𝑆 ) ∈ 2ndω ) )
45 44 rexlimivv ⊢ ( ∃ 𝑟 ∈ TopBases ∃ 𝑠 ∈ TopBases ( ( 𝑟 ≼ ω ∧ ( topGen ‘ 𝑟 ) = 𝑅 ) ∧ ( 𝑠 ≼ ω ∧ ( topGen ‘ 𝑠 ) = 𝑆 ) ) → ( 𝑅 ×t 𝑆 ) ∈ 2ndω )
46 3 45 sylbir ⊢ ( ( ∃ 𝑟 ∈ TopBases ( 𝑟 ≼ ω ∧ ( topGen ‘ 𝑟 ) = 𝑅 ) ∧ ∃ 𝑠 ∈ TopBases ( 𝑠 ≼ ω ∧ ( topGen ‘ 𝑠 ) = 𝑆 ) ) → ( 𝑅 ×t 𝑆 ) ∈ 2ndω )
47 1 2 46 syl2anb ⊢ ( ( 𝑅 ∈ 2ndω ∧ 𝑆 ∈ 2ndω ) → ( 𝑅 ×t 𝑆 ) ∈ 2ndω )