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* ) )
7 6 adantl 
 |-  ( ( ( ( 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 ) )
11 10 adantl 
 |-  ( ( ( ( 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 ) ) )
24 23 ad2antrr 
 |-  ( ( ( ( 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 ) ) )
25 8 16 22 24 mpbir3and 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( A W C /\ D X B ) ) /\ w e. ( C P D ) ) -> w e. ( A O B ) )
26 25 ex 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( A W C /\ D X B ) ) -> ( w e. ( C P D ) -> w e. ( A O B ) ) )
27 26 ssrdv 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( A W C /\ D X B ) ) -> ( C P D ) C_ ( A O B ) )