Theorem dishaus

Description: A discrete topology is Hausdorff. Morris, Topology without tears, p.72, ex. 13. (Contributed by FL, 24-Jun-2007) (Proof shortened by Mario Carneiro, 8-Apr-2015)

	Ref	Expression
Assertion	dishaus	⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Haus )

Proof

Step	Hyp	Ref	Expression
1		distop	⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Top )
2		simplrl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ∈ 𝐴 )
3	2	snssd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 ≠ 𝑦 ) → { 𝑥 } ⊆ 𝐴 )
4		vsnex	⊢ { 𝑥 } ∈ V
5	4	elpw	⊢ ( { 𝑥 } ∈ 𝒫 𝐴 ↔ { 𝑥 } ⊆ 𝐴 )
6	3 5	sylibr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 ≠ 𝑦 ) → { 𝑥 } ∈ 𝒫 𝐴 )
7		simplrr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑦 ∈ 𝐴 )
8	7	snssd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 ≠ 𝑦 ) → { 𝑦 } ⊆ 𝐴 )
9		vsnex	⊢ { 𝑦 } ∈ V
10	9	elpw	⊢ ( { 𝑦 } ∈ 𝒫 𝐴 ↔ { 𝑦 } ⊆ 𝐴 )
11	8 10	sylibr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 ≠ 𝑦 ) → { 𝑦 } ∈ 𝒫 𝐴 )
12		vsnid	⊢ 𝑥 ∈ { 𝑥 }
13	12	a1i	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ∈ { 𝑥 } )
14		vsnid	⊢ 𝑦 ∈ { 𝑦 }
15	14	a1i	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑦 ∈ { 𝑦 } )
16		disjsn2	⊢ ( 𝑥 ≠ 𝑦 → ( { 𝑥 } ∩ { 𝑦 } ) = ∅ )
17	16	adantl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( { 𝑥 } ∩ { 𝑦 } ) = ∅ )
18		eleq2	⊢ ( 𝑢 = { 𝑥 } → ( 𝑥 ∈ 𝑢 ↔ 𝑥 ∈ { 𝑥 } ) )
19		ineq1	⊢ ( 𝑢 = { 𝑥 } → ( 𝑢 ∩ 𝑣 ) = ( { 𝑥 } ∩ 𝑣 ) )
20	19	eqeq1d	⊢ ( 𝑢 = { 𝑥 } → ( ( 𝑢 ∩ 𝑣 ) = ∅ ↔ ( { 𝑥 } ∩ 𝑣 ) = ∅ ) )
21	18 20	3anbi13d	⊢ ( 𝑢 = { 𝑥 } → ( ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ↔ ( 𝑥 ∈ { 𝑥 } ∧ 𝑦 ∈ 𝑣 ∧ ( { 𝑥 } ∩ 𝑣 ) = ∅ ) ) )
22		eleq2	⊢ ( 𝑣 = { 𝑦 } → ( 𝑦 ∈ 𝑣 ↔ 𝑦 ∈ { 𝑦 } ) )
23		ineq2	⊢ ( 𝑣 = { 𝑦 } → ( { 𝑥 } ∩ 𝑣 ) = ( { 𝑥 } ∩ { 𝑦 } ) )
24	23	eqeq1d	⊢ ( 𝑣 = { 𝑦 } → ( ( { 𝑥 } ∩ 𝑣 ) = ∅ ↔ ( { 𝑥 } ∩ { 𝑦 } ) = ∅ ) )
25	22 24	3anbi23d	⊢ ( 𝑣 = { 𝑦 } → ( ( 𝑥 ∈ { 𝑥 } ∧ 𝑦 ∈ 𝑣 ∧ ( { 𝑥 } ∩ 𝑣 ) = ∅ ) ↔ ( 𝑥 ∈ { 𝑥 } ∧ 𝑦 ∈ { 𝑦 } ∧ ( { 𝑥 } ∩ { 𝑦 } ) = ∅ ) ) )
26	21 25	rspc2ev	⊢ ( ( { 𝑥 } ∈ 𝒫 𝐴 ∧ { 𝑦 } ∈ 𝒫 𝐴 ∧ ( 𝑥 ∈ { 𝑥 } ∧ 𝑦 ∈ { 𝑦 } ∧ ( { 𝑥 } ∩ { 𝑦 } ) = ∅ ) ) → ∃ 𝑢 ∈ 𝒫 𝐴 ∃ 𝑣 ∈ 𝒫 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) )
27	6 11 13 15 17 26	syl113anc	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 ≠ 𝑦 ) → ∃ 𝑢 ∈ 𝒫 𝐴 ∃ 𝑣 ∈ 𝒫 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) )
28	27	ex	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 ≠ 𝑦 → ∃ 𝑢 ∈ 𝒫 𝐴 ∃ 𝑣 ∈ 𝒫 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) )
29	28	ralrimivva	⊢ ( 𝐴 ∈ 𝑉 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → ∃ 𝑢 ∈ 𝒫 𝐴 ∃ 𝑣 ∈ 𝒫 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) )
30		unipw	⊢ ∪ 𝒫 𝐴 = 𝐴
31	30	eqcomi	⊢ 𝐴 = ∪ 𝒫 𝐴
32	31	ishaus	⊢ ( 𝒫 𝐴 ∈ Haus ↔ ( 𝒫 𝐴 ∈ Top ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → ∃ 𝑢 ∈ 𝒫 𝐴 ∃ 𝑣 ∈ 𝒫 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) )
33	1 29 32	sylanbrc	⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Haus )