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