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 
|- ( ( R e. 2ndc /\ S e. 2ndc ) -> ( R tX S ) e. 2ndc )

Proof

Step Hyp Ref Expression
1 is2ndc 
 |-  ( R e. 2ndc <-> E. r e. TopBases ( r ~<_ _om /\ ( topGen ` r ) = R ) )
2 is2ndc 
 |-  ( S e. 2ndc <-> E. s e. TopBases ( s ~<_ _om /\ ( topGen ` s ) = S ) )
3 reeanv 
 |-  ( E. r e. TopBases E. s e. TopBases ( ( r ~<_ _om /\ ( topGen ` r ) = R ) /\ ( s ~<_ _om /\ ( topGen ` s ) = S ) ) <-> ( E. r e. TopBases ( r ~<_ _om /\ ( topGen ` r ) = R ) /\ E. s e. TopBases ( s ~<_ _om /\ ( topGen ` s ) = S ) ) )
4 an4 
 |-  ( ( ( r ~<_ _om /\ ( topGen ` r ) = R ) /\ ( s ~<_ _om /\ ( topGen ` s ) = S ) ) <-> ( ( r ~<_ _om /\ s ~<_ _om ) /\ ( ( topGen ` r ) = R /\ ( topGen ` s ) = S ) ) )
5 txbasval 
 |-  ( ( r e. TopBases /\ s e. TopBases ) -> ( ( topGen ` r ) tX ( topGen ` s ) ) = ( r tX s ) )
6 eqid 
 |-  ran ( x e. r , y e. s |-> ( x X. y ) ) = ran ( x e. r , y e. s |-> ( x X. y ) )
7 6 txval 
 |-  ( ( r e. TopBases /\ s e. TopBases ) -> ( r tX s ) = ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )
8 5 7 eqtrd 
 |-  ( ( r e. TopBases /\ s e. TopBases ) -> ( ( topGen ` r ) tX ( topGen ` s ) ) = ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )
9 8 adantr 
 |-  ( ( ( r e. TopBases /\ s e. TopBases ) /\ ( r ~<_ _om /\ s ~<_ _om ) ) -> ( ( topGen ` r ) tX ( topGen ` s ) ) = ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )
10 6 txbas 
 |-  ( ( r e. TopBases /\ s e. TopBases ) -> ran ( x e. r , y e. s |-> ( x X. y ) ) e. TopBases )
11 10 adantr 
 |-  ( ( ( r e. TopBases /\ s e. TopBases ) /\ ( r ~<_ _om /\ s ~<_ _om ) ) -> ran ( x e. r , y e. s |-> ( x X. y ) ) e. TopBases )
12 omelon 
 |-  _om e. On
13 vex 
 |-  s e. _V
14 13 xpdom1 
 |-  ( r ~<_ _om -> ( r X. s ) ~<_ ( _om X. s ) )
15 omex 
 |-  _om e. _V
16 15 xpdom2 
 |-  ( s ~<_ _om -> ( _om X. s ) ~<_ ( _om X. _om ) )
17 domtr 
 |-  ( ( ( r X. s ) ~<_ ( _om X. s ) /\ ( _om X. s ) ~<_ ( _om X. _om ) ) -> ( r X. s ) ~<_ ( _om X. _om ) )
18 14 16 17 syl2an 
 |-  ( ( r ~<_ _om /\ s ~<_ _om ) -> ( r X. s ) ~<_ ( _om X. _om ) )
19 18 adantl 
 |-  ( ( ( r e. TopBases /\ s e. TopBases ) /\ ( r ~<_ _om /\ s ~<_ _om ) ) -> ( r X. s ) ~<_ ( _om X. _om ) )
20 xpomen 
 |-  ( _om X. _om ) ~~ _om
21 domentr 
 |-  ( ( ( r X. s ) ~<_ ( _om X. _om ) /\ ( _om X. _om ) ~~ _om ) -> ( r X. s ) ~<_ _om )
22 19 20 21 sylancl 
 |-  ( ( ( r e. TopBases /\ s e. TopBases ) /\ ( r ~<_ _om /\ s ~<_ _om ) ) -> ( r X. s ) ~<_ _om )
23 ondomen 
 |-  ( ( _om e. On /\ ( r X. s ) ~<_ _om ) -> ( r X. s ) e. dom card )
24 12 22 23 sylancr 
 |-  ( ( ( r e. TopBases /\ s e. TopBases ) /\ ( r ~<_ _om /\ s ~<_ _om ) ) -> ( r X. s ) e. dom card )
25 eqid 
 |-  ( x e. r , y e. s |-> ( x X. y ) ) = ( x e. r , y e. s |-> ( x X. y ) )
26 vex 
 |-  x e. _V
27 vex 
 |-  y e. _V
28 26 27 xpex 
 |-  ( x X. y ) e. _V
29 25 28 fnmpoi 
 |-  ( x e. r , y e. s |-> ( x X. y ) ) Fn ( r X. s )
30 29 a1i 
 |-  ( ( ( r e. TopBases /\ s e. TopBases ) /\ ( r ~<_ _om /\ s ~<_ _om ) ) -> ( x e. r , y e. s |-> ( x X. y ) ) Fn ( r X. s ) )
31 dffn4 
 |-  ( ( x e. r , y e. s |-> ( x X. y ) ) Fn ( r X. s ) <-> ( x e. r , y e. s |-> ( x X. y ) ) : ( r X. s ) -onto-> ran ( x e. r , y e. s |-> ( x X. y ) ) )
32 30 31 sylib 
 |-  ( ( ( r e. TopBases /\ s e. TopBases ) /\ ( r ~<_ _om /\ s ~<_ _om ) ) -> ( x e. r , y e. s |-> ( x X. y ) ) : ( r X. s ) -onto-> ran ( x e. r , y e. s |-> ( x X. y ) ) )
33 fodomnum 
 |-  ( ( r X. s ) e. dom card -> ( ( x e. r , y e. s |-> ( x X. y ) ) : ( r X. s ) -onto-> ran ( x e. r , y e. s |-> ( x X. y ) ) -> ran ( x e. r , y e. s |-> ( x X. y ) ) ~<_ ( r X. s ) ) )
34 24 32 33 sylc 
 |-  ( ( ( r e. TopBases /\ s e. TopBases ) /\ ( r ~<_ _om /\ s ~<_ _om ) ) -> ran ( x e. r , y e. s |-> ( x X. y ) ) ~<_ ( r X. s ) )
35 domtr 
 |-  ( ( ran ( x e. r , y e. s |-> ( x X. y ) ) ~<_ ( r X. s ) /\ ( r X. s ) ~<_ _om ) -> ran ( x e. r , y e. s |-> ( x X. y ) ) ~<_ _om )
36 34 22 35 syl2anc 
 |-  ( ( ( r e. TopBases /\ s e. TopBases ) /\ ( r ~<_ _om /\ s ~<_ _om ) ) -> ran ( x e. r , y e. s |-> ( x X. y ) ) ~<_ _om )
37 2ndci 
 |-  ( ( ran ( x e. r , y e. s |-> ( x X. y ) ) e. TopBases /\ ran ( x e. r , y e. s |-> ( x X. y ) ) ~<_ _om ) -> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) e. 2ndc )
38 11 36 37 syl2anc 
 |-  ( ( ( r e. TopBases /\ s e. TopBases ) /\ ( r ~<_ _om /\ s ~<_ _om ) ) -> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) e. 2ndc )
39 9 38 eqeltrd 
 |-  ( ( ( r e. TopBases /\ s e. TopBases ) /\ ( r ~<_ _om /\ s ~<_ _om ) ) -> ( ( topGen ` r ) tX ( topGen ` s ) ) e. 2ndc )
40 oveq12 
 |-  ( ( ( topGen ` r ) = R /\ ( topGen ` s ) = S ) -> ( ( topGen ` r ) tX ( topGen ` s ) ) = ( R tX S ) )
41 40 eleq1d 
 |-  ( ( ( topGen ` r ) = R /\ ( topGen ` s ) = S ) -> ( ( ( topGen ` r ) tX ( topGen ` s ) ) e. 2ndc <-> ( R tX S ) e. 2ndc ) )
42 39 41 syl5ibcom 
 |-  ( ( ( r e. TopBases /\ s e. TopBases ) /\ ( r ~<_ _om /\ s ~<_ _om ) ) -> ( ( ( topGen ` r ) = R /\ ( topGen ` s ) = S ) -> ( R tX S ) e. 2ndc ) )
43 42 expimpd 
 |-  ( ( r e. TopBases /\ s e. TopBases ) -> ( ( ( r ~<_ _om /\ s ~<_ _om ) /\ ( ( topGen ` r ) = R /\ ( topGen ` s ) = S ) ) -> ( R tX S ) e. 2ndc ) )
44 4 43 biimtrid 
 |-  ( ( r e. TopBases /\ s e. TopBases ) -> ( ( ( r ~<_ _om /\ ( topGen ` r ) = R ) /\ ( s ~<_ _om /\ ( topGen ` s ) = S ) ) -> ( R tX S ) e. 2ndc ) )
45 44 rexlimivv 
 |-  ( E. r e. TopBases E. s e. TopBases ( ( r ~<_ _om /\ ( topGen ` r ) = R ) /\ ( s ~<_ _om /\ ( topGen ` s ) = S ) ) -> ( R tX S ) e. 2ndc )
46 3 45 sylbir 
 |-  ( ( E. r e. TopBases ( r ~<_ _om /\ ( topGen ` r ) = R ) /\ E. s e. TopBases ( s ~<_ _om /\ ( topGen ` s ) = S ) ) -> ( R tX S ) e. 2ndc )
47 1 2 46 syl2anb 
 |-  ( ( R e. 2ndc /\ S e. 2ndc ) -> ( R tX S ) e. 2ndc )