Metamath Proof Explorer

Theorem ist0-3

Description: The predicate "is a T_0 space" expressed in more familiar terms. (Contributed by Jeff Hankins, 1-Feb-2010)

Ref Expression
Assertion ist0-3 ⊢ J ∈ TopOn ⁡ X → J ∈ Kol2 ↔ ∀ x ∈ X ∀ y ∈ X x ≠ y → ∃ o ∈ J x ∈ o ∧ ¬ y ∈ o ∨ ¬ x ∈ o ∧ y ∈ o

Proof

Step Hyp Ref Expression
1 ist0-2 ⊢ J ∈ TopOn ⁡ X → J ∈ Kol2 ↔ ∀ x ∈ X ∀ y ∈ X ∀ o ∈ J x ∈ o ↔ y ∈ o → x = y
2 con34b ⊢ ∀ o ∈ J x ∈ o ↔ y ∈ o → x = y ↔ ¬ x = y → ¬ ∀ o ∈ J x ∈ o ↔ y ∈ o
3 df-ne ⊢ x ≠ y ↔ ¬ x = y
4 xor ⊢ ¬ x ∈ o ↔ y ∈ o ↔ x ∈ o ∧ ¬ y ∈ o ∨ y ∈ o ∧ ¬ x ∈ o
5 ancom ⊢ y ∈ o ∧ ¬ x ∈ o ↔ ¬ x ∈ o ∧ y ∈ o
6 5 orbi2i ⊢ x ∈ o ∧ ¬ y ∈ o ∨ y ∈ o ∧ ¬ x ∈ o ↔ x ∈ o ∧ ¬ y ∈ o ∨ ¬ x ∈ o ∧ y ∈ o
7 4 6 bitri ⊢ ¬ x ∈ o ↔ y ∈ o ↔ x ∈ o ∧ ¬ y ∈ o ∨ ¬ x ∈ o ∧ y ∈ o
8 7 rexbii ⊢ ∃ o ∈ J ¬ x ∈ o ↔ y ∈ o ↔ ∃ o ∈ J x ∈ o ∧ ¬ y ∈ o ∨ ¬ x ∈ o ∧ y ∈ o
9 rexnal ⊢ ∃ o ∈ J ¬ x ∈ o ↔ y ∈ o ↔ ¬ ∀ o ∈ J x ∈ o ↔ y ∈ o
10 8 9 bitr3i ⊢ ∃ o ∈ J x ∈ o ∧ ¬ y ∈ o ∨ ¬ x ∈ o ∧ y ∈ o ↔ ¬ ∀ o ∈ J x ∈ o ↔ y ∈ o
11 3 10 imbi12i ⊢ x ≠ y → ∃ o ∈ J x ∈ o ∧ ¬ y ∈ o ∨ ¬ x ∈ o ∧ y ∈ o ↔ ¬ x = y → ¬ ∀ o ∈ J x ∈ o ↔ y ∈ o
12 2 11 bitr4i ⊢ ∀ o ∈ J x ∈ o ↔ y ∈ o → x = y ↔ x ≠ y → ∃ o ∈ J x ∈ o ∧ ¬ y ∈ o ∨ ¬ x ∈ o ∧ y ∈ o
13 12 2ralbii ⊢ ∀ x ∈ X ∀ y ∈ X ∀ o ∈ J x ∈ o ↔ y ∈ o → x = y ↔ ∀ x ∈ X ∀ y ∈ X x ≠ y → ∃ o ∈ J x ∈ o ∧ ¬ y ∈ o ∨ ¬ x ∈ o ∧ y ∈ o
14 1 13 syl6bb ⊢ J ∈ TopOn ⁡ X → J ∈ Kol2 ↔ ∀ x ∈ X ∀ y ∈ X x ≠ y → ∃ o ∈ J x ∈ o ∧ ¬ y ∈ o ∨ ¬ x ∈ o ∧ y ∈ o