Metamath Proof Explorer


Theorem ist0-2

Description: The predicate "is a T_0 space". (Contributed by Mario Carneiro, 24-Aug-2015)

Ref Expression
Assertion ist0-2 ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Kol2 ↔ ∀ 𝑥𝑋𝑦𝑋 ( ∀ 𝑜𝐽 ( 𝑥𝑜𝑦𝑜 ) → 𝑥 = 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 topontop ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
2 eqid 𝐽 = 𝐽
3 2 ist0 ( 𝐽 ∈ Kol2 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 𝐽𝑦 𝐽 ( ∀ 𝑜𝐽 ( 𝑥𝑜𝑦𝑜 ) → 𝑥 = 𝑦 ) ) )
4 3 baib ( 𝐽 ∈ Top → ( 𝐽 ∈ Kol2 ↔ ∀ 𝑥 𝐽𝑦 𝐽 ( ∀ 𝑜𝐽 ( 𝑥𝑜𝑦𝑜 ) → 𝑥 = 𝑦 ) ) )
5 1 4 syl ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Kol2 ↔ ∀ 𝑥 𝐽𝑦 𝐽 ( ∀ 𝑜𝐽 ( 𝑥𝑜𝑦𝑜 ) → 𝑥 = 𝑦 ) ) )
6 toponuni ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = 𝐽 )
7 6 raleqdv ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ∀ 𝑦𝑋 ( ∀ 𝑜𝐽 ( 𝑥𝑜𝑦𝑜 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 𝐽 ( ∀ 𝑜𝐽 ( 𝑥𝑜𝑦𝑜 ) → 𝑥 = 𝑦 ) ) )
8 6 7 raleqbidv ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ∀ 𝑥𝑋𝑦𝑋 ( ∀ 𝑜𝐽 ( 𝑥𝑜𝑦𝑜 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 𝐽𝑦 𝐽 ( ∀ 𝑜𝐽 ( 𝑥𝑜𝑦𝑜 ) → 𝑥 = 𝑦 ) ) )
9 5 8 bitr4d ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Kol2 ↔ ∀ 𝑥𝑋𝑦𝑋 ( ∀ 𝑜𝐽 ( 𝑥𝑜𝑦𝑜 ) → 𝑥 = 𝑦 ) ) )