# 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 syl6ibr ( 𝑦𝐴 → ( 𝑥𝐴 → ( 𝑥𝑦 ) ∈ 𝒫 𝐴 ) )
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 )