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 ⊢ J ∈ TopOn ⁡ X ∧ KQ ⁡ J ∈ Fre ∧ A ∈ X ∧ B ∈ X → ∀ o ∈ J A ∈ o → B ∈ o → ∀ o ∈ J A ∈ o ↔ B ∈ o

Proof

Step Hyp Ref Expression
1 eqid ⊢ z ∈ X ⟼ w ∈ J | z ∈ w = z ∈ X ⟼ w ∈ J | z ∈ w
2 1 isr0 ⊢ J ∈ TopOn ⁡ X → KQ ⁡ J ∈ Fre ↔ ∀ x ∈ X ∀ y ∈ X ∀ o ∈ J x ∈ o → y ∈ o → ∀ o ∈ J x ∈ o ↔ y ∈ o
3 2 biimpa ⊢ J ∈ TopOn ⁡ X ∧ KQ ⁡ J ∈ Fre → ∀ x ∈ X ∀ y ∈ X ∀ o ∈ J x ∈ o → y ∈ o → ∀ o ∈ J x ∈ o ↔ y ∈ o
4 eleq1 ⊢ x = A → x ∈ o ↔ A ∈ o
5 4 imbi1d ⊢ x = A → x ∈ o → y ∈ o ↔ A ∈ o → y ∈ o
6 5 ralbidv ⊢ x = A → ∀ o ∈ J x ∈ o → y ∈ o ↔ ∀ o ∈ J A ∈ o → y ∈ o
7 4 bibi1d ⊢ x = A → x ∈ o ↔ y ∈ o ↔ A ∈ o ↔ y ∈ o
8 7 ralbidv ⊢ x = A → ∀ o ∈ J x ∈ o ↔ y ∈ o ↔ ∀ o ∈ J A ∈ o ↔ y ∈ o
9 6 8 imbi12d ⊢ x = A → ∀ o ∈ J x ∈ o → y ∈ o → ∀ o ∈ J x ∈ o ↔ y ∈ o ↔ ∀ o ∈ J A ∈ o → y ∈ o → ∀ o ∈ J A ∈ o ↔ y ∈ o
10 eleq1 ⊢ y = B → y ∈ o ↔ B ∈ o
11 10 imbi2d ⊢ y = B → A ∈ o → y ∈ o ↔ A ∈ o → B ∈ o
12 11 ralbidv ⊢ y = B → ∀ o ∈ J A ∈ o → y ∈ o ↔ ∀ o ∈ J A ∈ o → B ∈ o
13 10 bibi2d ⊢ y = B → A ∈ o ↔ y ∈ o ↔ A ∈ o ↔ B ∈ o
14 13 ralbidv ⊢ y = B → ∀ o ∈ J A ∈ o ↔ y ∈ o ↔ ∀ o ∈ J A ∈ o ↔ B ∈ o
15 12 14 imbi12d ⊢ y = B → ∀ o ∈ J A ∈ o → y ∈ o → ∀ o ∈ J A ∈ o ↔ y ∈ o ↔ ∀ o ∈ J A ∈ o → B ∈ o → ∀ o ∈ J A ∈ o ↔ B ∈ o
16 9 15 rspc2v ⊢ A ∈ X ∧ B ∈ X → ∀ x ∈ X ∀ y ∈ X ∀ o ∈ J x ∈ o → y ∈ o → ∀ o ∈ J x ∈ o ↔ y ∈ o → ∀ o ∈ J A ∈ o → B ∈ o → ∀ o ∈ J A ∈ o ↔ B ∈ o
17 3 16 mpan9 ⊢ J ∈ TopOn ⁡ X ∧ KQ ⁡ J ∈ Fre ∧ A ∈ X ∧ B ∈ X → ∀ o ∈ J A ∈ o → B ∈ o → ∀ o ∈ J A ∈ o ↔ B ∈ o