Metamath Proof Explorer

Theorem ordtcld3

Description: A closed interval [ A , B ] is closed. (Contributed by Mario Carneiro, 3-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 ordttopon.3 ⊢ X = dom ⁡ R
2 inrab ⊢ x ∈ X | A R x ∩ x ∈ X | x R B = x ∈ X | A R x ∧ x R B
3 1 ordtcld2 ⊢ R ∈ V ∧ A ∈ X → x ∈ X | A R x ∈ Clsd ⁡ ordTop ⁡ R
4 3 3adant3 ⊢ R ∈ V ∧ A ∈ X ∧ B ∈ X → x ∈ X | A R x ∈ Clsd ⁡ ordTop ⁡ R
5 1 ordtcld1 ⊢ R ∈ V ∧ B ∈ X → x ∈ X | x R B ∈ Clsd ⁡ ordTop ⁡ R
6 incld ⊢ x ∈ X | A R x ∈ Clsd ⁡ ordTop ⁡ R ∧ x ∈ X | x R B ∈ Clsd ⁡ ordTop ⁡ R → x ∈ X | A R x ∩ x ∈ X | x R B ∈ Clsd ⁡ ordTop ⁡ R
7 4 5 6 3imp3i2an ⊢ R ∈ V ∧ A ∈ X ∧ B ∈ X → x ∈ X | A R x ∩ x ∈ X | x R B ∈ Clsd ⁡ ordTop ⁡ R
8 2 7 eqeltrrid ⊢ R ∈ V ∧ A ∈ X ∧ B ∈ X → x ∈ X | A R x ∧ x R B ∈ Clsd ⁡ ordTop ⁡ R