Metamath Proof Explorer

Theorem ordtopn3

Description: An open interval ( A , B ) is open. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypothesis ordttopon.3 ⊢ X = dom ⁡ R
Assertion ordtopn3 ⊢ R ∈ V ∧ A ∈ X ∧ B ∈ X → x ∈ X | ¬ x R A ∧ ¬ B R x ∈ ordTop ⁡ R

Proof

Step Hyp Ref Expression
1 ordttopon.3 ⊢ X = dom ⁡ R
2 inrab ⊢ x ∈ X | ¬ x R A ∩ x ∈ X | ¬ B R x = x ∈ X | ¬ x R A ∧ ¬ B R x
3 1 ordttopon ⊢ R ∈ V → ordTop ⁡ R ∈ TopOn ⁡ X
4 3 3ad2ant1 ⊢ R ∈ V ∧ A ∈ X ∧ B ∈ X → ordTop ⁡ R ∈ TopOn ⁡ X
5 topontop ⊢ ordTop ⁡ R ∈ TopOn ⁡ X → ordTop ⁡ R ∈ Top
6 4 5 syl ⊢ R ∈ V ∧ A ∈ X ∧ B ∈ X → ordTop ⁡ R ∈ Top
7 1 ordtopn1 ⊢ R ∈ V ∧ A ∈ X → x ∈ X | ¬ x R A ∈ ordTop ⁡ R
8 7 3adant3 ⊢ R ∈ V ∧ A ∈ X ∧ B ∈ X → x ∈ X | ¬ x R A ∈ ordTop ⁡ R
9 1 ordtopn2 ⊢ R ∈ V ∧ B ∈ X → x ∈ X | ¬ B R x ∈ ordTop ⁡ R
10 9 3adant2 ⊢ R ∈ V ∧ A ∈ X ∧ B ∈ X → x ∈ X | ¬ B R x ∈ ordTop ⁡ R
11 inopn ⊢ ordTop ⁡ R ∈ Top ∧ x ∈ X | ¬ x R A ∈ ordTop ⁡ R ∧ x ∈ X | ¬ B R x ∈ ordTop ⁡ R → x ∈ X | ¬ x R A ∩ x ∈ X | ¬ B R x ∈ ordTop ⁡ R
12 6 8 10 11 syl3anc ⊢ R ∈ V ∧ A ∈ X ∧ B ∈ X → x ∈ X | ¬ x R A ∩ x ∈ X | ¬ B R x ∈ ordTop ⁡ R
13 2 12 eqeltrrid ⊢ R ∈ V ∧ A ∈ X ∧ B ∈ X → x ∈ X | ¬ x R A ∧ ¬ B R x ∈ ordTop ⁡ R