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 ⊢ A ∈ V → 𝒫 A ∈ Top

Proof

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