This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )