This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem distop

Description: The discrete topology on a set A . Part of Example 2 in Munkres p. 77. (Contributed by FL, 17-Jul-2006) (Revised by Mario Carneiro, 19-Mar-2015)

Ref Expression
Assertion distop ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Top )

Proof

Step Hyp Ref Expression
1 uniss ⊢ ( 𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ⊆ ∪ 𝒫 𝐴 )
2 unipw ⊢ ∪ 𝒫 𝐴 = 𝐴
3 1 2 sseqtrdi ⊢ ( 𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ⊆ 𝐴 )
4 vuniex ⊢ ∪ 𝑥 ∈ V
5 4 elpw ⊢ ( ∪ 𝑥 ∈ 𝒫 𝐴 ↔ ∪ 𝑥 ⊆ 𝐴 )
6 3 5 sylibr ⊢ ( 𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ∈ 𝒫 𝐴 )
7 6 ax-gen ⊢ ∀ 𝑥 ( 𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ∈ 𝒫 𝐴 )
8 7 a1i ⊢ ( 𝐴 ∈ 𝑉 → ∀ 𝑥 ( 𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ∈ 𝒫 𝐴 ) )
9 velpw ⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
10 velpw ⊢ ( 𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 ⊆ 𝐴 )
11 ssinss1 ⊢ ( 𝑥 ⊆ 𝐴 → ( 𝑥 ∩ 𝑦 ) ⊆ 𝐴 )
12 11 a1i ⊢ ( 𝑦 ⊆ 𝐴 → ( 𝑥 ⊆ 𝐴 → ( 𝑥 ∩ 𝑦 ) ⊆ 𝐴 ) )
13 vex ⊢ 𝑦 ∈ V
14 13 inex2 ⊢ ( 𝑥 ∩ 𝑦 ) ∈ V
15 14 elpw ⊢ ( ( 𝑥 ∩ 𝑦 ) ∈ 𝒫 𝐴 ↔ ( 𝑥 ∩ 𝑦 ) ⊆ 𝐴 )
16 12 15 imbitrrdi ⊢ ( 𝑦 ⊆ 𝐴 → ( 𝑥 ⊆ 𝐴 → ( 𝑥 ∩ 𝑦 ) ∈ 𝒫 𝐴 ) )
17 10 16 sylbi ⊢ ( 𝑦 ∈ 𝒫 𝐴 → ( 𝑥 ⊆ 𝐴 → ( 𝑥 ∩ 𝑦 ) ∈ 𝒫 𝐴 ) )
18 17 com12 ⊢ ( 𝑥 ⊆ 𝐴 → ( 𝑦 ∈ 𝒫 𝐴 → ( 𝑥 ∩ 𝑦 ) ∈ 𝒫 𝐴 ) )
19 9 18 sylbi ⊢ ( 𝑥 ∈ 𝒫 𝐴 → ( 𝑦 ∈ 𝒫 𝐴 → ( 𝑥 ∩ 𝑦 ) ∈ 𝒫 𝐴 ) )
20 19 ralrimiv ⊢ ( 𝑥 ∈ 𝒫 𝐴 → ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑥 ∩ 𝑦 ) ∈ 𝒫 𝐴 )
21 20 rgen ⊢ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑥 ∩ 𝑦 ) ∈ 𝒫 𝐴
22 21 a1i ⊢ ( 𝐴 ∈ 𝑉 → ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑥 ∩ 𝑦 ) ∈ 𝒫 𝐴 )
23 pwexg ⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V )
24 istopg ⊢ ( 𝒫 𝐴 ∈ V → ( 𝒫 𝐴 ∈ Top ↔ ( ∀ 𝑥 ( 𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ∈ 𝒫 𝐴 ) ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑥 ∩ 𝑦 ) ∈ 𝒫 𝐴 ) ) )
25 23 24 syl ⊢ ( 𝐴 ∈ 𝑉 → ( 𝒫 𝐴 ∈ Top ↔ ( ∀ 𝑥 ( 𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ∈ 𝒫 𝐴 ) ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑥 ∩ 𝑦 ) ∈ 𝒫 𝐴 ) ) )
26 8 22 25 mpbir2and ⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Top )