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 e. V /\ P e. X ) -> { x e. X | x R P } e. ( Clsd ` ( ordTop ` R ) ) )

Proof

Step Hyp Ref Expression
1 ordttopon.3
 |-  X = dom R
2 ssrab2
 |-  { x e. X | x R P } C_ X
3 1 ordttopon
 |-  ( R e. V -> ( ordTop ` R ) e. ( TopOn ` X ) )
4 3 adantr
 |-  ( ( R e. V /\ P e. X ) -> ( ordTop ` R ) e. ( TopOn ` X ) )
5 toponuni
 |-  ( ( ordTop ` R ) e. ( TopOn ` X ) -> X = U. ( ordTop ` R ) )
6 4 5 syl
 |-  ( ( R e. V /\ P e. X ) -> X = U. ( ordTop ` R ) )
7 2 6 sseqtrid
 |-  ( ( R e. V /\ P e. X ) -> { x e. X | x R P } C_ U. ( ordTop ` R ) )
8 notrab
 |-  ( X \ { x e. X | x R P } ) = { x e. X | -. x R P }
9 6 difeq1d
 |-  ( ( R e. V /\ P e. X ) -> ( X \ { x e. X | x R P } ) = ( U. ( ordTop ` R ) \ { x e. X | x R P } ) )
10 8 9 eqtr3id
 |-  ( ( R e. V /\ P e. X ) -> { x e. X | -. x R P } = ( U. ( ordTop ` R ) \ { x e. X | x R P } ) )
11 1 ordtopn1
 |-  ( ( R e. V /\ P e. X ) -> { x e. X | -. x R P } e. ( ordTop ` R ) )
12 10 11 eqeltrrd
 |-  ( ( R e. V /\ P e. X ) -> ( U. ( ordTop ` R ) \ { x e. X | x R P } ) e. ( ordTop ` R ) )
13 topontop
 |-  ( ( ordTop ` R ) e. ( TopOn ` X ) -> ( ordTop ` R ) e. Top )
14 eqid
 |-  U. ( ordTop ` R ) = U. ( ordTop ` R )
15 14 iscld
 |-  ( ( ordTop ` R ) e. Top -> ( { x e. X | x R P } e. ( Clsd ` ( ordTop ` R ) ) <-> ( { x e. X | x R P } C_ U. ( ordTop ` R ) /\ ( U. ( ordTop ` R ) \ { x e. X | x R P } ) e. ( ordTop ` R ) ) ) )
16 4 13 15 3syl
 |-  ( ( R e. V /\ P e. X ) -> ( { x e. X | x R P } e. ( Clsd ` ( ordTop ` R ) ) <-> ( { x e. X | x R P } C_ U. ( ordTop ` R ) /\ ( U. ( ordTop ` R ) \ { x e. X | x R P } ) e. ( ordTop ` R ) ) ) )
17 7 12 16 mpbir2and
 |-  ( ( R e. V /\ P e. X ) -> { x e. X | x R P } e. ( Clsd ` ( ordTop ` R ) ) )