Metamath Proof Explorer

Theorem txdis

Description: The topological product of discrete spaces is discrete. (Contributed by Mario Carneiro, 14-Aug-2015)

Ref Expression
Assertion txdis 
|- ( ( A e. V /\ B e. W ) -> ( ~P A tX ~P B ) = ~P ( A X. B ) )

Proof

Step Hyp Ref Expression
1 distop 
 |-  ( A e. V -> ~P A e. Top )
2 distop 
 |-  ( B e. W -> ~P B e. Top )
3 unipw 
 |-  U. ~P A = A
4 3 eqcomi 
 |-  A = U. ~P A
5 unipw 
 |-  U. ~P B = B
6 5 eqcomi 
 |-  B = U. ~P B
7 4 6 txuni 
 |-  ( ( ~P A e. Top /\ ~P B e. Top ) -> ( A X. B ) = U. ( ~P A tX ~P B ) )
8 1 2 7 syl2an 
 |-  ( ( A e. V /\ B e. W ) -> ( A X. B ) = U. ( ~P A tX ~P B ) )
9 eqimss2 
 |-  ( ( A X. B ) = U. ( ~P A tX ~P B ) -> U. ( ~P A tX ~P B ) C_ ( A X. B ) )
10 8 9 syl 
 |-  ( ( A e. V /\ B e. W ) -> U. ( ~P A tX ~P B ) C_ ( A X. B ) )
11 sspwuni 
 |-  ( ( ~P A tX ~P B ) C_ ~P ( A X. B ) <-> U. ( ~P A tX ~P B ) C_ ( A X. B ) )
12 10 11 sylibr 
 |-  ( ( A e. V /\ B e. W ) -> ( ~P A tX ~P B ) C_ ~P ( A X. B ) )
13 elelpwi 
 |-  ( ( y e. x /\ x e. ~P ( A X. B ) ) -> y e. ( A X. B ) )
14 13 adantl 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( y e. x /\ x e. ~P ( A X. B ) ) ) -> y e. ( A X. B ) )
15 xp1st 
 |-  ( y e. ( A X. B ) -> ( 1st ` y ) e. A )
16 snelpwi 
 |-  ( ( 1st ` y ) e. A -> { ( 1st ` y ) } e. ~P A )
17 14 15 16 3syl 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( y e. x /\ x e. ~P ( A X. B ) ) ) -> { ( 1st ` y ) } e. ~P A )
18 xp2nd 
 |-  ( y e. ( A X. B ) -> ( 2nd ` y ) e. B )
19 snelpwi 
 |-  ( ( 2nd ` y ) e. B -> { ( 2nd ` y ) } e. ~P B )
20 14 18 19 3syl 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( y e. x /\ x e. ~P ( A X. B ) ) ) -> { ( 2nd ` y ) } e. ~P B )
21 vsnid 
 |-  y e. { y }
22 1st2nd2 
 |-  ( y e. ( A X. B ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
23 14 22 syl 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( y e. x /\ x e. ~P ( A X. B ) ) ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
24 23 sneqd 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( y e. x /\ x e. ~P ( A X. B ) ) ) -> { y } = { <. ( 1st ` y ) , ( 2nd ` y ) >. } )
25 21 24 eleqtrid 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( y e. x /\ x e. ~P ( A X. B ) ) ) -> y e. { <. ( 1st ` y ) , ( 2nd ` y ) >. } )
26 simprl 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( y e. x /\ x e. ~P ( A X. B ) ) ) -> y e. x )
27 23 26 eqeltrrd 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( y e. x /\ x e. ~P ( A X. B ) ) ) -> <. ( 1st ` y ) , ( 2nd ` y ) >. e. x )
28 27 snssd 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( y e. x /\ x e. ~P ( A X. B ) ) ) -> { <. ( 1st ` y ) , ( 2nd ` y ) >. } C_ x )
29 xpeq1 
 |-  ( z = { ( 1st ` y ) } -> ( z X. w ) = ( { ( 1st ` y ) } X. w ) )
30 29 eleq2d 
 |-  ( z = { ( 1st ` y ) } -> ( y e. ( z X. w ) <-> y e. ( { ( 1st ` y ) } X. w ) ) )
31 29 sseq1d 
 |-  ( z = { ( 1st ` y ) } -> ( ( z X. w ) C_ x <-> ( { ( 1st ` y ) } X. w ) C_ x ) )
32 30 31 anbi12d 
 |-  ( z = { ( 1st ` y ) } -> ( ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) <-> ( y e. ( { ( 1st ` y ) } X. w ) /\ ( { ( 1st ` y ) } X. w ) C_ x ) ) )
33 xpeq2 
 |-  ( w = { ( 2nd ` y ) } -> ( { ( 1st ` y ) } X. w ) = ( { ( 1st ` y ) } X. { ( 2nd ` y ) } ) )
34 fvex 
 |-  ( 1st ` y ) e. _V
35 fvex 
 |-  ( 2nd ` y ) e. _V
36 34 35 xpsn 
 |-  ( { ( 1st ` y ) } X. { ( 2nd ` y ) } ) = { <. ( 1st ` y ) , ( 2nd ` y ) >. }
37 33 36 eqtrdi 
 |-  ( w = { ( 2nd ` y ) } -> ( { ( 1st ` y ) } X. w ) = { <. ( 1st ` y ) , ( 2nd ` y ) >. } )
38 37 eleq2d 
 |-  ( w = { ( 2nd ` y ) } -> ( y e. ( { ( 1st ` y ) } X. w ) <-> y e. { <. ( 1st ` y ) , ( 2nd ` y ) >. } ) )
39 37 sseq1d 
 |-  ( w = { ( 2nd ` y ) } -> ( ( { ( 1st ` y ) } X. w ) C_ x <-> { <. ( 1st ` y ) , ( 2nd ` y ) >. } C_ x ) )
40 38 39 anbi12d 
 |-  ( w = { ( 2nd ` y ) } -> ( ( y e. ( { ( 1st ` y ) } X. w ) /\ ( { ( 1st ` y ) } X. w ) C_ x ) <-> ( y e. { <. ( 1st ` y ) , ( 2nd ` y ) >. } /\ { <. ( 1st ` y ) , ( 2nd ` y ) >. } C_ x ) ) )
41 32 40 rspc2ev 
 |-  ( ( { ( 1st ` y ) } e. ~P A /\ { ( 2nd ` y ) } e. ~P B /\ ( y e. { <. ( 1st ` y ) , ( 2nd ` y ) >. } /\ { <. ( 1st ` y ) , ( 2nd ` y ) >. } C_ x ) ) -> E. z e. ~P A E. w e. ~P B ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) )
42 17 20 25 28 41 syl112anc 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( y e. x /\ x e. ~P ( A X. B ) ) ) -> E. z e. ~P A E. w e. ~P B ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) )
43 42 expr 
 |-  ( ( ( A e. V /\ B e. W ) /\ y e. x ) -> ( x e. ~P ( A X. B ) -> E. z e. ~P A E. w e. ~P B ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) )
44 43 ralrimdva 
 |-  ( ( A e. V /\ B e. W ) -> ( x e. ~P ( A X. B ) -> A. y e. x E. z e. ~P A E. w e. ~P B ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) )
45 eltx 
 |-  ( ( ~P A e. Top /\ ~P B e. Top ) -> ( x e. ( ~P A tX ~P B ) <-> A. y e. x E. z e. ~P A E. w e. ~P B ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) )
46 1 2 45 syl2an 
 |-  ( ( A e. V /\ B e. W ) -> ( x e. ( ~P A tX ~P B ) <-> A. y e. x E. z e. ~P A E. w e. ~P B ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) )
47 44 46 sylibrd 
 |-  ( ( A e. V /\ B e. W ) -> ( x e. ~P ( A X. B ) -> x e. ( ~P A tX ~P B ) ) )
48 47 ssrdv 
 |-  ( ( A e. V /\ B e. W ) -> ~P ( A X. B ) C_ ( ~P A tX ~P B ) )
49 12 48 eqssd 
 |-  ( ( A e. V /\ B e. W ) -> ( ~P A tX ~P B ) = ~P ( A X. B ) )