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