Theorem ordtcld3

Description: A closed interval [ A , B ] is closed. (Contributed by Mario Carneiro, 3-Sep-2015)

	Ref	Expression
Hypothesis	ordttopon.3	|- X = dom R
Assertion	ordtcld3	|- ( ( R e. V /\ A e. X /\ B e. X ) -> { x e. X | ( A R x /\ x R B ) } e. ( Clsd ` ( ordTop ` R ) ) )

Proof

Step	Hyp	Ref	Expression
1		ordttopon.3	|- X = dom R
2		inrab	|- ( { x e. X | A R x } i^i { x e. X | x R B } ) = { x e. X | ( A R x /\ x R B ) }
3	1	ordtcld2	|- ( ( R e. V /\ A e. X ) -> { x e. X | A R x } e. ( Clsd ` ( ordTop ` R ) ) )
4	3	3adant3	|- ( ( R e. V /\ A e. X /\ B e. X ) -> { x e. X | A R x } e. ( Clsd ` ( ordTop ` R ) ) )
5	1	ordtcld1	|- ( ( R e. V /\ B e. X ) -> { x e. X | x R B } e. ( Clsd ` ( ordTop ` R ) ) )
6		incld	|- ( ( { x e. X | A R x } e. ( Clsd ` ( ordTop ` R ) ) /\ { x e. X | x R B } e. ( Clsd ` ( ordTop ` R ) ) ) -> ( { x e. X | A R x } i^i { x e. X | x R B } ) e. ( Clsd ` ( ordTop ` R ) ) )
7	4 5 6	3imp3i2an	|- ( ( R e. V /\ A e. X /\ B e. X ) -> ( { x e. X | A R x } i^i { x e. X | x R B } ) e. ( Clsd ` ( ordTop ` R ) ) )
8	2 7	eqeltrrid	|- ( ( R e. V /\ A e. X /\ B e. X ) -> { x e. X | ( A R x /\ x R B ) } e. ( Clsd ` ( ordTop ` R ) ) )