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

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 ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Kol2 ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ≠ 𝑦 → ∃ 𝑜 ∈ 𝐽 ( ( 𝑥 ∈ 𝑜 ∧ ¬ 𝑦 ∈ 𝑜 ) ∨ ( ¬ 𝑥 ∈ 𝑜 ∧ 𝑦 ∈ 𝑜 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ist0-2 ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Kol2 ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) )
2 con34b ⊢ ( ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ↔ ( ¬ 𝑥 = 𝑦 → ¬ ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) ) )
3 df-ne ⊢ ( 𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦 )
4 xor ⊢ ( ¬ ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) ↔ ( ( 𝑥 ∈ 𝑜 ∧ ¬ 𝑦 ∈ 𝑜 ) ∨ ( 𝑦 ∈ 𝑜 ∧ ¬ 𝑥 ∈ 𝑜 ) ) )
5 ancom ⊢ ( ( 𝑦 ∈ 𝑜 ∧ ¬ 𝑥 ∈ 𝑜 ) ↔ ( ¬ 𝑥 ∈ 𝑜 ∧ 𝑦 ∈ 𝑜 ) )
6 5 orbi2i ⊢ ( ( ( 𝑥 ∈ 𝑜 ∧ ¬ 𝑦 ∈ 𝑜 ) ∨ ( 𝑦 ∈ 𝑜 ∧ ¬ 𝑥 ∈ 𝑜 ) ) ↔ ( ( 𝑥 ∈ 𝑜 ∧ ¬ 𝑦 ∈ 𝑜 ) ∨ ( ¬ 𝑥 ∈ 𝑜 ∧ 𝑦 ∈ 𝑜 ) ) )
7 4 6 bitri ⊢ ( ¬ ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) ↔ ( ( 𝑥 ∈ 𝑜 ∧ ¬ 𝑦 ∈ 𝑜 ) ∨ ( ¬ 𝑥 ∈ 𝑜 ∧ 𝑦 ∈ 𝑜 ) ) )
8 7 rexbii ⊢ ( ∃ 𝑜 ∈ 𝐽 ¬ ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) ↔ ∃ 𝑜 ∈ 𝐽 ( ( 𝑥 ∈ 𝑜 ∧ ¬ 𝑦 ∈ 𝑜 ) ∨ ( ¬ 𝑥 ∈ 𝑜 ∧ 𝑦 ∈ 𝑜 ) ) )
9 rexnal ⊢ ( ∃ 𝑜 ∈ 𝐽 ¬ ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) ↔ ¬ ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) )
10 8 9 bitr3i ⊢ ( ∃ 𝑜 ∈ 𝐽 ( ( 𝑥 ∈ 𝑜 ∧ ¬ 𝑦 ∈ 𝑜 ) ∨ ( ¬ 𝑥 ∈ 𝑜 ∧ 𝑦 ∈ 𝑜 ) ) ↔ ¬ ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) )
11 3 10 imbi12i ⊢ ( ( 𝑥 ≠ 𝑦 → ∃ 𝑜 ∈ 𝐽 ( ( 𝑥 ∈ 𝑜 ∧ ¬ 𝑦 ∈ 𝑜 ) ∨ ( ¬ 𝑥 ∈ 𝑜 ∧ 𝑦 ∈ 𝑜 ) ) ) ↔ ( ¬ 𝑥 = 𝑦 → ¬ ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) ) )
12 2 11 bitr4i ⊢ ( ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ↔ ( 𝑥 ≠ 𝑦 → ∃ 𝑜 ∈ 𝐽 ( ( 𝑥 ∈ 𝑜 ∧ ¬ 𝑦 ∈ 𝑜 ) ∨ ( ¬ 𝑥 ∈ 𝑜 ∧ 𝑦 ∈ 𝑜 ) ) ) )
13 12 2ralbii ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ≠ 𝑦 → ∃ 𝑜 ∈ 𝐽 ( ( 𝑥 ∈ 𝑜 ∧ ¬ 𝑦 ∈ 𝑜 ) ∨ ( ¬ 𝑥 ∈ 𝑜 ∧ 𝑦 ∈ 𝑜 ) ) ) )
14 1 13 bitrdi ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Kol2 ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ≠ 𝑦 → ∃ 𝑜 ∈ 𝐽 ( ( 𝑥 ∈ 𝑜 ∧ ¬ 𝑦 ∈ 𝑜 ) ∨ ( ¬ 𝑥 ∈ 𝑜 ∧ 𝑦 ∈ 𝑜 ) ) ) ) )