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 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜 ) → ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 ↔ 𝐵 ∈ 𝑜 ) ) )