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 )