Metamath Proof Explorer

Theorem iooss1

Description: Subset relationship for open intervals of extended reals. (Contributed by NM, 7-Feb-2007) (Revised by Mario Carneiro, 20-Feb-2015)

		Ref	Expression
	Assertion	iooss1	\|- ( ( A e. RR* /\ A <_ B ) -> ( B (,) C ) C_ ( A (,) C ) )

Step	Hyp	Ref	Expression
1		df-ioo	\|- (,) = ( x e. RR* , y e. RR* \|-> { z e. RR* \| ( x < z /\ z < y ) } )
2		xrlelttr	\|- ( ( A e. RR* /\ B e. RR* /\ w e. RR* ) -> ( ( A <_ B /\ B < w ) -> A < w ) )
3	1 1 2	ixxss1	\|- ( ( A e. RR* /\ A <_ B ) -> ( B (,) C ) C_ ( A (,) C ) )

Step

Hyp

Ref

Expression

 |-  (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )

 |-  ( ( A e. RR* /\ B e. RR* /\ w e. RR* ) -> ( ( A <_ B /\ B < w ) -> A < w ) )

1 1 2

 |-  ( ( A e. RR* /\ A <_ B ) -> ( B (,) C ) C_ ( A (,) C ) )