This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

Step Hyp Ref Expression
1 ordttopon.3 
 |-  X = dom R
2 ssrab2 
 |-  { x e. X | P R x } 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 | P R x } C_ U. ( ordTop ` R ) )
8 notrab 
 |-  ( X \ { x e. X | P R x } ) = { x e. X | -. P R x }
9 6 difeq1d 
 |-  ( ( R e. V /\ P e. X ) -> ( X \ { x e. X | P R x } ) = ( U. ( ordTop ` R ) \ { x e. X | P R x } ) )
10 8 9 eqtr3id 
 |-  ( ( R e. V /\ P e. X ) -> { x e. X | -. P R x } = ( U. ( ordTop ` R ) \ { x e. X | P R x } ) )
11 1 ordtopn2 
 |-  ( ( R e. V /\ P e. X ) -> { x e. X | -. P R x } e. ( ordTop ` R ) )
12 10 11 eqeltrrd 
 |-  ( ( R e. V /\ P e. X ) -> ( U. ( ordTop ` R ) \ { x e. X | P R x } ) 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 | P R x } e. ( Clsd ` ( ordTop ` R ) ) <-> ( { x e. X | P R x } C_ U. ( ordTop ` R ) /\ ( U. ( ordTop ` R ) \ { x e. X | P R x } ) e. ( ordTop ` R ) ) ) )
16 4 13 15 3syl 
 |-  ( ( R e. V /\ P e. X ) -> ( { x e. X | P R x } e. ( Clsd ` ( ordTop ` R ) ) <-> ( { x e. X | P R x } C_ U. ( ordTop ` R ) /\ ( U. ( ordTop ` R ) \ { x e. X | P R x } ) e. ( ordTop ` R ) ) ) )
17 7 12 16 mpbir2and 
 |-  ( ( R e. V /\ P e. X ) -> { x e. X | P R x } e. ( Clsd ` ( ordTop ` R ) ) )