Metamath Proof Explorer

Theorem ordtcld1

Description: A downward ray ( -oo , P ] is closed. (Contributed by Mario Carneiro, 3-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 ordttopon.3 ⊢ X = dom ⁡ R
2 ssrab2 ⊢ x ∈ X | x R P ⊆ X
3 1 ordttopon ⊢ R ∈ V → ordTop ⁡ R ∈ TopOn ⁡ X
4 3 adantr ⊢ R ∈ V ∧ P ∈ X → ordTop ⁡ R ∈ TopOn ⁡ X
5 toponuni ⊢ ordTop ⁡ R ∈ TopOn ⁡ X → X = ⋃ ordTop ⁡ R
6 4 5 syl ⊢ R ∈ V ∧ P ∈ X → X = ⋃ ordTop ⁡ R
7 2 6 sseqtrid ⊢ R ∈ V ∧ P ∈ X → x ∈ X | x R P ⊆ ⋃ ordTop ⁡ R
8 notrab ⊢ X ∖ x ∈ X | x R P = x ∈ X | ¬ x R P
9 6 difeq1d ⊢ R ∈ V ∧ P ∈ X → X ∖ x ∈ X | x R P = ⋃ ordTop ⁡ R ∖ x ∈ X | x R P
10 8 9 syl5eqr ⊢ R ∈ V ∧ P ∈ X → x ∈ X | ¬ x R P = ⋃ ordTop ⁡ R ∖ x ∈ X | x R P
11 1 ordtopn1 ⊢ R ∈ V ∧ P ∈ X → x ∈ X | ¬ x R P ∈ ordTop ⁡ R
12 10 11 eqeltrrd ⊢ R ∈ V ∧ P ∈ X → ⋃ ordTop ⁡ R ∖ x ∈ X | x R P ∈ ordTop ⁡ R
13 topontop ⊢ ordTop ⁡ R ∈ TopOn ⁡ X → ordTop ⁡ R ∈ Top
14 eqid ⊢ ⋃ ordTop ⁡ R = ⋃ ordTop ⁡ R
15 14 iscld ⊢ ordTop ⁡ R ∈ Top → x ∈ X | x R P ∈ Clsd ⁡ ordTop ⁡ R ↔ x ∈ X | x R P ⊆ ⋃ ordTop ⁡ R ∧ ⋃ ordTop ⁡ R ∖ x ∈ X | x R P ∈ ordTop ⁡ R
16 4 13 15 3syl ⊢ R ∈ V ∧ P ∈ X → x ∈ X | x R P ∈ Clsd ⁡ ordTop ⁡ R ↔ x ∈ X | x R P ⊆ ⋃ ordTop ⁡ R ∧ ⋃ ordTop ⁡ R ∖ x ∈ X | x R P ∈ ordTop ⁡ R
17 7 12 16 mpbir2and ⊢ R ∈ V ∧ P ∈ X → x ∈ X | x R P ∈ Clsd ⁡ ordTop ⁡ R