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 ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝒫 𝐴 ×t 𝒫 𝐵 ) = 𝒫 ( 𝐴 × 𝐵 ) )

Proof

Step Hyp Ref Expression
1 distop ( 𝐴𝑉 → 𝒫 𝐴 ∈ Top )
2 distop ( 𝐵𝑊 → 𝒫 𝐵 ∈ Top )
3 unipw 𝒫 𝐴 = 𝐴
4 3 eqcomi 𝐴 = 𝒫 𝐴
5 unipw 𝒫 𝐵 = 𝐵
6 5 eqcomi 𝐵 = 𝒫 𝐵
7 4 6 txuni ( ( 𝒫 𝐴 ∈ Top ∧ 𝒫 𝐵 ∈ Top ) → ( 𝐴 × 𝐵 ) = ( 𝒫 𝐴 ×t 𝒫 𝐵 ) )
8 1 2 7 syl2an ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝐴 × 𝐵 ) = ( 𝒫 𝐴 ×t 𝒫 𝐵 ) )
9 eqimss2 ( ( 𝐴 × 𝐵 ) = ( 𝒫 𝐴 ×t 𝒫 𝐵 ) → ( 𝒫 𝐴 ×t 𝒫 𝐵 ) ⊆ ( 𝐴 × 𝐵 ) )
10 8 9 syl ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝒫 𝐴 ×t 𝒫 𝐵 ) ⊆ ( 𝐴 × 𝐵 ) )
11 sspwuni ( ( 𝒫 𝐴 ×t 𝒫 𝐵 ) ⊆ 𝒫 ( 𝐴 × 𝐵 ) ↔ ( 𝒫 𝐴 ×t 𝒫 𝐵 ) ⊆ ( 𝐴 × 𝐵 ) )
12 10 11 sylibr ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝒫 𝐴 ×t 𝒫 𝐵 ) ⊆ 𝒫 ( 𝐴 × 𝐵 ) )
13 elelpwi ( ( 𝑦𝑥𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) → 𝑦 ∈ ( 𝐴 × 𝐵 ) )
14 13 adantl ( ( ( 𝐴𝑉𝐵𝑊 ) ∧ ( 𝑦𝑥𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ) → 𝑦 ∈ ( 𝐴 × 𝐵 ) )
15 xp1st ( 𝑦 ∈ ( 𝐴 × 𝐵 ) → ( 1st𝑦 ) ∈ 𝐴 )
16 snelpwi ( ( 1st𝑦 ) ∈ 𝐴 → { ( 1st𝑦 ) } ∈ 𝒫 𝐴 )
17 14 15 16 3syl ( ( ( 𝐴𝑉𝐵𝑊 ) ∧ ( 𝑦𝑥𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ) → { ( 1st𝑦 ) } ∈ 𝒫 𝐴 )
18 xp2nd ( 𝑦 ∈ ( 𝐴 × 𝐵 ) → ( 2nd𝑦 ) ∈ 𝐵 )
19 snelpwi ( ( 2nd𝑦 ) ∈ 𝐵 → { ( 2nd𝑦 ) } ∈ 𝒫 𝐵 )
20 14 18 19 3syl ( ( ( 𝐴𝑉𝐵𝑊 ) ∧ ( 𝑦𝑥𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ) → { ( 2nd𝑦 ) } ∈ 𝒫 𝐵 )
21 vsnid 𝑦 ∈ { 𝑦 }
22 1st2nd2 ( 𝑦 ∈ ( 𝐴 × 𝐵 ) → 𝑦 = ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ )
23 14 22 syl ( ( ( 𝐴𝑉𝐵𝑊 ) ∧ ( 𝑦𝑥𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ) → 𝑦 = ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ )
24 23 sneqd ( ( ( 𝐴𝑉𝐵𝑊 ) ∧ ( 𝑦𝑥𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ) → { 𝑦 } = { ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ } )
25 21 24 eleqtrid ( ( ( 𝐴𝑉𝐵𝑊 ) ∧ ( 𝑦𝑥𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ) → 𝑦 ∈ { ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ } )
26 simprl ( ( ( 𝐴𝑉𝐵𝑊 ) ∧ ( 𝑦𝑥𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ) → 𝑦𝑥 )
27 23 26 eqeltrrd ( ( ( 𝐴𝑉𝐵𝑊 ) ∧ ( 𝑦𝑥𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ) → ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ ∈ 𝑥 )
28 27 snssd ( ( ( 𝐴𝑉𝐵𝑊 ) ∧ ( 𝑦𝑥𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ) → { ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ } ⊆ 𝑥 )
29 xpeq1 ( 𝑧 = { ( 1st𝑦 ) } → ( 𝑧 × 𝑤 ) = ( { ( 1st𝑦 ) } × 𝑤 ) )
30 29 eleq2d ( 𝑧 = { ( 1st𝑦 ) } → ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ↔ 𝑦 ∈ ( { ( 1st𝑦 ) } × 𝑤 ) ) )
31 29 sseq1d ( 𝑧 = { ( 1st𝑦 ) } → ( ( 𝑧 × 𝑤 ) ⊆ 𝑥 ↔ ( { ( 1st𝑦 ) } × 𝑤 ) ⊆ 𝑥 ) )
32 30 31 anbi12d ( 𝑧 = { ( 1st𝑦 ) } → ( ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ↔ ( 𝑦 ∈ ( { ( 1st𝑦 ) } × 𝑤 ) ∧ ( { ( 1st𝑦 ) } × 𝑤 ) ⊆ 𝑥 ) ) )
33 xpeq2 ( 𝑤 = { ( 2nd𝑦 ) } → ( { ( 1st𝑦 ) } × 𝑤 ) = ( { ( 1st𝑦 ) } × { ( 2nd𝑦 ) } ) )
34 fvex ( 1st𝑦 ) ∈ V
35 fvex ( 2nd𝑦 ) ∈ V
36 34 35 xpsn ( { ( 1st𝑦 ) } × { ( 2nd𝑦 ) } ) = { ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ }
37 33 36 eqtrdi ( 𝑤 = { ( 2nd𝑦 ) } → ( { ( 1st𝑦 ) } × 𝑤 ) = { ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ } )
38 37 eleq2d ( 𝑤 = { ( 2nd𝑦 ) } → ( 𝑦 ∈ ( { ( 1st𝑦 ) } × 𝑤 ) ↔ 𝑦 ∈ { ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ } ) )
39 37 sseq1d ( 𝑤 = { ( 2nd𝑦 ) } → ( ( { ( 1st𝑦 ) } × 𝑤 ) ⊆ 𝑥 ↔ { ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ } ⊆ 𝑥 ) )
40 38 39 anbi12d ( 𝑤 = { ( 2nd𝑦 ) } → ( ( 𝑦 ∈ ( { ( 1st𝑦 ) } × 𝑤 ) ∧ ( { ( 1st𝑦 ) } × 𝑤 ) ⊆ 𝑥 ) ↔ ( 𝑦 ∈ { ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ } ∧ { ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ } ⊆ 𝑥 ) ) )
41 32 40 rspc2ev ( ( { ( 1st𝑦 ) } ∈ 𝒫 𝐴 ∧ { ( 2nd𝑦 ) } ∈ 𝒫 𝐵 ∧ ( 𝑦 ∈ { ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ } ∧ { ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ } ⊆ 𝑥 ) ) → ∃ 𝑧 ∈ 𝒫 𝐴𝑤 ∈ 𝒫 𝐵 ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) )
42 17 20 25 28 41 syl112anc ( ( ( 𝐴𝑉𝐵𝑊 ) ∧ ( 𝑦𝑥𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ) → ∃ 𝑧 ∈ 𝒫 𝐴𝑤 ∈ 𝒫 𝐵 ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) )
43 42 expr ( ( ( 𝐴𝑉𝐵𝑊 ) ∧ 𝑦𝑥 ) → ( 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) → ∃ 𝑧 ∈ 𝒫 𝐴𝑤 ∈ 𝒫 𝐵 ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) )
44 43 ralrimdva ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) → ∀ 𝑦𝑥𝑧 ∈ 𝒫 𝐴𝑤 ∈ 𝒫 𝐵 ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) )
45 eltx ( ( 𝒫 𝐴 ∈ Top ∧ 𝒫 𝐵 ∈ Top ) → ( 𝑥 ∈ ( 𝒫 𝐴 ×t 𝒫 𝐵 ) ↔ ∀ 𝑦𝑥𝑧 ∈ 𝒫 𝐴𝑤 ∈ 𝒫 𝐵 ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) )
46 1 2 45 syl2an ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝑥 ∈ ( 𝒫 𝐴 ×t 𝒫 𝐵 ) ↔ ∀ 𝑦𝑥𝑧 ∈ 𝒫 𝐴𝑤 ∈ 𝒫 𝐵 ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) )
47 44 46 sylibrd ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) → 𝑥 ∈ ( 𝒫 𝐴 ×t 𝒫 𝐵 ) ) )
48 47 ssrdv ( ( 𝐴𝑉𝐵𝑊 ) → 𝒫 ( 𝐴 × 𝐵 ) ⊆ ( 𝒫 𝐴 ×t 𝒫 𝐵 ) )
49 12 48 eqssd ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝒫 𝐴 ×t 𝒫 𝐵 ) = 𝒫 ( 𝐴 × 𝐵 ) )