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

Metamath Proof Explorer

Theorem r0sep

Description: The separation property of an R_0 space. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion r0sep ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜 ) → ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 ↔ 𝐵 ∈ 𝑜 ) ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝐽 ∣ 𝑧 ∈ 𝑤 } ) = ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝐽 ∣ 𝑧 ∈ 𝑤 } )
2 1 isr0 ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ( KQ ‘ 𝐽 ) ∈ Fre ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) ) ) )
3 2 biimpa ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) ) )
4 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝑜 ↔ 𝐴 ∈ 𝑜 ) )
5 4 imbi1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) ↔ ( 𝐴 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) ) )
6 5 ralbidv ⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) ↔ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) ) )
7 4 bibi1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) ↔ ( 𝐴 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) ) )
8 7 ralbidv ⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) ↔ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) ) )
9 6 8 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) ) ↔ ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) ) ) )
10 eleq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 ∈ 𝑜 ↔ 𝐵 ∈ 𝑜 ) )
11 10 imbi2d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) ↔ ( 𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜 ) ) )
12 11 ralbidv ⊢ ( 𝑦 = 𝐵 → ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) ↔ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜 ) ) )
13 10 bibi2d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) ↔ ( 𝐴 ∈ 𝑜 ↔ 𝐵 ∈ 𝑜 ) ) )
14 13 ralbidv ⊢ ( 𝑦 = 𝐵 → ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) ↔ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 ↔ 𝐵 ∈ 𝑜 ) ) )
15 12 14 imbi12d ⊢ ( 𝑦 = 𝐵 → ( ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) ) ↔ ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜 ) → ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 ↔ 𝐵 ∈ 𝑜 ) ) ) )
16 9 15 rspc2v ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜 ) → ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 ↔ 𝐵 ∈ 𝑜 ) ) ) )
17 3 16 mpan9 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜 ) → ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 ↔ 𝐵 ∈ 𝑜 ) ) )