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 V B W 𝒫 A × t 𝒫 B = 𝒫 A × B

Proof

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