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