Theorem haust1

Description: A Hausdorff space is a T_1 space. (Contributed by FL, 11-Jun-2007) (Proof shortened by Mario Carneiro, 24-Aug-2015)

	Ref	Expression
Assertion	haust1	⊢ ( 𝐽 ∈ Haus → 𝐽 ∈ Fre )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
2	1	hausnei	⊢ ( ( 𝐽 ∈ Haus ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ∧ 𝑥 ≠ 𝑦 ) ) → ∃ 𝑧 ∈ 𝐽 ∃ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) )
3		simprr1	⊢ ( ( ( ( 𝐽 ∈ Haus ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑧 ∈ 𝐽 ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) ) → 𝑥 ∈ 𝑧 )
4		noel	⊢ ¬ 𝑦 ∈ ∅
5		simprr3	⊢ ( ( ( ( 𝐽 ∈ Haus ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑧 ∈ 𝐽 ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) ) → ( 𝑧 ∩ 𝑤 ) = ∅ )
6	5	eleq2d	⊢ ( ( ( ( 𝐽 ∈ Haus ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑧 ∈ 𝐽 ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) ) → ( 𝑦 ∈ ( 𝑧 ∩ 𝑤 ) ↔ 𝑦 ∈ ∅ ) )
7	4 6	mtbiri	⊢ ( ( ( ( 𝐽 ∈ Haus ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑧 ∈ 𝐽 ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) ) → ¬ 𝑦 ∈ ( 𝑧 ∩ 𝑤 ) )
8		simprr2	⊢ ( ( ( ( 𝐽 ∈ Haus ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑧 ∈ 𝐽 ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) ) → 𝑦 ∈ 𝑤 )
9		elin	⊢ ( 𝑦 ∈ ( 𝑧 ∩ 𝑤 ) ↔ ( 𝑦 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ) )
10	9	simplbi2com	⊢ ( 𝑦 ∈ 𝑤 → ( 𝑦 ∈ 𝑧 → 𝑦 ∈ ( 𝑧 ∩ 𝑤 ) ) )
11	8 10	syl	⊢ ( ( ( ( 𝐽 ∈ Haus ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑧 ∈ 𝐽 ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) ) → ( 𝑦 ∈ 𝑧 → 𝑦 ∈ ( 𝑧 ∩ 𝑤 ) ) )
12	7 11	mtod	⊢ ( ( ( ( 𝐽 ∈ Haus ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑧 ∈ 𝐽 ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) ) → ¬ 𝑦 ∈ 𝑧 )
13	3 12	jca	⊢ ( ( ( ( 𝐽 ∈ Haus ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑧 ∈ 𝐽 ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) ) → ( 𝑥 ∈ 𝑧 ∧ ¬ 𝑦 ∈ 𝑧 ) )
14	13	rexlimdvaa	⊢ ( ( ( 𝐽 ∈ Haus ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑧 ∈ 𝐽 ) → ( ∃ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) → ( 𝑥 ∈ 𝑧 ∧ ¬ 𝑦 ∈ 𝑧 ) ) )
15	14	reximdva	⊢ ( ( 𝐽 ∈ Haus ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ∧ 𝑥 ≠ 𝑦 ) ) → ( ∃ 𝑧 ∈ 𝐽 ∃ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) → ∃ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ∧ ¬ 𝑦 ∈ 𝑧 ) ) )
16	2 15	mpd	⊢ ( ( 𝐽 ∈ Haus ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ∧ 𝑥 ≠ 𝑦 ) ) → ∃ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ∧ ¬ 𝑦 ∈ 𝑧 ) )
17		rexanali	⊢ ( ∃ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ∧ ¬ 𝑦 ∈ 𝑧 ) ↔ ¬ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧 ) )
18	16 17	sylib	⊢ ( ( 𝐽 ∈ Haus ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ∧ 𝑥 ≠ 𝑦 ) ) → ¬ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧 ) )
19	18	3exp2	⊢ ( 𝐽 ∈ Haus → ( 𝑥 ∈ ∪ 𝐽 → ( 𝑦 ∈ ∪ 𝐽 → ( 𝑥 ≠ 𝑦 → ¬ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧 ) ) ) ) )
20	19	imp32	⊢ ( ( 𝐽 ∈ Haus ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → ( 𝑥 ≠ 𝑦 → ¬ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧 ) ) )
21	20	necon4ad	⊢ ( ( 𝐽 ∈ Haus ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → ( ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧 ) → 𝑥 = 𝑦 ) )
22	21	ralrimivva	⊢ ( 𝐽 ∈ Haus → ∀ 𝑥 ∈ ∪ 𝐽 ∀ 𝑦 ∈ ∪ 𝐽 ( ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧 ) → 𝑥 = 𝑦 ) )
23		haustop	⊢ ( 𝐽 ∈ Haus → 𝐽 ∈ Top )
24		toptopon2	⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
25	23 24	sylib	⊢ ( 𝐽 ∈ Haus → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
26		ist1-2	⊢ ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) → ( 𝐽 ∈ Fre ↔ ∀ 𝑥 ∈ ∪ 𝐽 ∀ 𝑦 ∈ ∪ 𝐽 ( ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧 ) → 𝑥 = 𝑦 ) ) )
27	25 26	syl	⊢ ( 𝐽 ∈ Haus → ( 𝐽 ∈ Fre ↔ ∀ 𝑥 ∈ ∪ 𝐽 ∀ 𝑦 ∈ ∪ 𝐽 ( ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧 ) → 𝑥 = 𝑦 ) ) )
28	22 27	mpbird	⊢ ( 𝐽 ∈ Haus → 𝐽 ∈ Fre )