Metamath Proof Explorer

Theorem ordtcld2

Description: An upward ray [ P , +oo ) is closed. (Contributed by Mario Carneiro, 3-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 ordttopon.3 ⊢ X = dom ⁡ R
2 ssrab2 ⊢ x ∈ X | P R x ⊆ 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 | P R x ⊆ ⋃ ordTop ⁡ R
8 notrab ⊢ X ∖ x ∈ X | P R x = x ∈ X | ¬ P R x
9 6 difeq1d ⊢ R ∈ V ∧ P ∈ X → X ∖ x ∈ X | P R x = ⋃ ordTop ⁡ R ∖ x ∈ X | P R x
10 8 9 eqtr3id ⊢ R ∈ V ∧ P ∈ X → x ∈ X | ¬ P R x = ⋃ ordTop ⁡ R ∖ x ∈ X | P R x
11 1 ordtopn2 ⊢ R ∈ V ∧ P ∈ X → x ∈ X | ¬ P R x ∈ ordTop ⁡ R
12 10 11 eqeltrrd ⊢ R ∈ V ∧ P ∈ X → ⋃ ordTop ⁡ R ∖ x ∈ X | P R x ∈ 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 | P R x ∈ Clsd ⁡ ordTop ⁡ R ↔ x ∈ X | P R x ⊆ ⋃ ordTop ⁡ R ∧ ⋃ ordTop ⁡ R ∖ x ∈ X | P R x ∈ ordTop ⁡ R
16 4 13 15 3syl ⊢ R ∈ V ∧ P ∈ X → x ∈ X | P R x ∈ Clsd ⁡ ordTop ⁡ R ↔ x ∈ X | P R x ⊆ ⋃ ordTop ⁡ R ∧ ⋃ ordTop ⁡ R ∖ x ∈ X | P R x ∈ ordTop ⁡ R
17 7 12 16 mpbir2and ⊢ R ∈ V ∧ P ∈ X → x ∈ X | P R x ∈ Clsd ⁡ ordTop ⁡ R