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=domR
Assertion ordtcld3 RVAXBXxX|ARxxRBClsdordTopR

Proof

Step Hyp Ref Expression
1 ordttopon.3 X=domR
2 inrab xX|ARxxX|xRB=xX|ARxxRB
3 1 ordtcld2 RVAXxX|ARxClsdordTopR
4 3 3adant3 RVAXBXxX|ARxClsdordTopR
5 1 ordtcld1 RVBXxX|xRBClsdordTopR
6 incld xX|ARxClsdordTopRxX|xRBClsdordTopRxX|ARxxX|xRBClsdordTopR
7 4 5 6 3imp3i2an RVAXBXxX|ARxxX|xRBClsdordTopR
8 2 7 eqeltrrid RVAXBXxX|ARxxRBClsdordTopR