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 eqtr3id 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