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

Metamath Proof Explorer

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