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