# Metamath Proof Explorer

## Theorem ixxss12

Description: Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 20-Feb-2015) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Hypotheses ixx.1
`|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )`
ixxss12.2
`|- P = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x T z /\ z U y ) } )`
ixxss12.3
`|- ( ( A e. RR* /\ C e. RR* /\ w e. RR* ) -> ( ( A W C /\ C T w ) -> A R w ) )`
ixxss12.4
`|- ( ( w e. RR* /\ D e. RR* /\ B e. RR* ) -> ( ( w U D /\ D X B ) -> w S B ) )`
Assertion ixxss12
`|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( A W C /\ D X B ) ) -> ( C P D ) C_ ( A O B ) )`

### Proof

Step Hyp Ref Expression
1 ixx.1
` |-  O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )`
2 ixxss12.2
` |-  P = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x T z /\ z U y ) } )`
3 ixxss12.3
` |-  ( ( A e. RR* /\ C e. RR* /\ w e. RR* ) -> ( ( A W C /\ C T w ) -> A R w ) )`
4 ixxss12.4
` |-  ( ( w e. RR* /\ D e. RR* /\ B e. RR* ) -> ( ( w U D /\ D X B ) -> w S B ) )`
5 2 elixx3g
` |-  ( w e. ( C P D ) <-> ( ( C e. RR* /\ D e. RR* /\ w e. RR* ) /\ ( C T w /\ w U D ) ) )`
6 5 simplbi
` |-  ( w e. ( C P D ) -> ( C e. RR* /\ D e. RR* /\ w e. RR* ) )`
` |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( A W C /\ D X B ) ) /\ w e. ( C P D ) ) -> ( C e. RR* /\ D e. RR* /\ w e. RR* ) )`
8 7 simp3d
` |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( A W C /\ D X B ) ) /\ w e. ( C P D ) ) -> w e. RR* )`
9 simplrl
` |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( A W C /\ D X B ) ) /\ w e. ( C P D ) ) -> A W C )`
10 5 simprbi
` |-  ( w e. ( C P D ) -> ( C T w /\ w U D ) )`
` |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( A W C /\ D X B ) ) /\ w e. ( C P D ) ) -> ( C T w /\ w U D ) )`
12 11 simpld
` |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( A W C /\ D X B ) ) /\ w e. ( C P D ) ) -> C T w )`
13 simplll
` |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( A W C /\ D X B ) ) /\ w e. ( C P D ) ) -> A e. RR* )`
14 7 simp1d
` |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( A W C /\ D X B ) ) /\ w e. ( C P D ) ) -> C e. RR* )`
15 13 14 8 3 syl3anc
` |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( A W C /\ D X B ) ) /\ w e. ( C P D ) ) -> ( ( A W C /\ C T w ) -> A R w ) )`
16 9 12 15 mp2and
` |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( A W C /\ D X B ) ) /\ w e. ( C P D ) ) -> A R w )`
17 11 simprd
` |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( A W C /\ D X B ) ) /\ w e. ( C P D ) ) -> w U D )`
18 simplrr
` |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( A W C /\ D X B ) ) /\ w e. ( C P D ) ) -> D X B )`
19 7 simp2d
` |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( A W C /\ D X B ) ) /\ w e. ( C P D ) ) -> D e. RR* )`
20 simpllr
` |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( A W C /\ D X B ) ) /\ w e. ( C P D ) ) -> B e. RR* )`
21 8 19 20 4 syl3anc
` |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( A W C /\ D X B ) ) /\ w e. ( C P D ) ) -> ( ( w U D /\ D X B ) -> w S B ) )`
22 17 18 21 mp2and
` |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( A W C /\ D X B ) ) /\ w e. ( C P D ) ) -> w S B )`
23 1 elixx1
` |-  ( ( A e. RR* /\ B e. RR* ) -> ( w e. ( A O B ) <-> ( w e. RR* /\ A R w /\ w S B ) ) )`
` |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( A W C /\ D X B ) ) /\ w e. ( C P D ) ) -> ( w e. ( A O B ) <-> ( w e. RR* /\ A R w /\ w S B ) ) )`
` |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( A W C /\ D X B ) ) /\ w e. ( C P D ) ) -> w e. ( A O B ) )`
` |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( A W C /\ D X B ) ) -> ( w e. ( C P D ) -> w e. ( A O B ) ) )`
` |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( A W C /\ D X B ) ) -> ( C P D ) C_ ( A O B ) )`