Metamath Proof Explorer

Theorem ixxss1

Description: Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013) (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 ) } )
ixxss1.2 
|- P = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x T z /\ z S y ) } )
ixxss1.3 
|- ( ( A e. RR* /\ B e. RR* /\ w e. RR* ) -> ( ( A W B /\ B T w ) -> A R w ) )
Assertion ixxss1 
|- ( ( A e. RR* /\ A W B ) -> ( B P C ) C_ ( A O C ) )

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 ixxss1.2 
 |-  P = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x T z /\ z S y ) } )
3 ixxss1.3 
 |-  ( ( A e. RR* /\ B e. RR* /\ w e. RR* ) -> ( ( A W B /\ B T w ) -> A R w ) )
4 2 elixx3g 
 |-  ( w e. ( B P C ) <-> ( ( B e. RR* /\ C e. RR* /\ w e. RR* ) /\ ( B T w /\ w S C ) ) )
5 4 simplbi 
 |-  ( w e. ( B P C ) -> ( B e. RR* /\ C e. RR* /\ w e. RR* ) )
6 5 adantl 
 |-  ( ( ( A e. RR* /\ A W B ) /\ w e. ( B P C ) ) -> ( B e. RR* /\ C e. RR* /\ w e. RR* ) )
7 6 simp3d 
 |-  ( ( ( A e. RR* /\ A W B ) /\ w e. ( B P C ) ) -> w e. RR* )
8 simplr 
 |-  ( ( ( A e. RR* /\ A W B ) /\ w e. ( B P C ) ) -> A W B )
9 4 simprbi 
 |-  ( w e. ( B P C ) -> ( B T w /\ w S C ) )
10 9 adantl 
 |-  ( ( ( A e. RR* /\ A W B ) /\ w e. ( B P C ) ) -> ( B T w /\ w S C ) )
11 10 simpld 
 |-  ( ( ( A e. RR* /\ A W B ) /\ w e. ( B P C ) ) -> B T w )
12 simpll 
 |-  ( ( ( A e. RR* /\ A W B ) /\ w e. ( B P C ) ) -> A e. RR* )
13 6 simp1d 
 |-  ( ( ( A e. RR* /\ A W B ) /\ w e. ( B P C ) ) -> B e. RR* )
14 12 13 7 3 syl3anc 
 |-  ( ( ( A e. RR* /\ A W B ) /\ w e. ( B P C ) ) -> ( ( A W B /\ B T w ) -> A R w ) )
15 8 11 14 mp2and 
 |-  ( ( ( A e. RR* /\ A W B ) /\ w e. ( B P C ) ) -> A R w )
16 10 simprd 
 |-  ( ( ( A e. RR* /\ A W B ) /\ w e. ( B P C ) ) -> w S C )
17 6 simp2d 
 |-  ( ( ( A e. RR* /\ A W B ) /\ w e. ( B P C ) ) -> C e. RR* )
18 1 elixx1 
 |-  ( ( A e. RR* /\ C e. RR* ) -> ( w e. ( A O C ) <-> ( w e. RR* /\ A R w /\ w S C ) ) )
19 12 17 18 syl2anc 
 |-  ( ( ( A e. RR* /\ A W B ) /\ w e. ( B P C ) ) -> ( w e. ( A O C ) <-> ( w e. RR* /\ A R w /\ w S C ) ) )
20 7 15 16 19 mpbir3and 
 |-  ( ( ( A e. RR* /\ A W B ) /\ w e. ( B P C ) ) -> w e. ( A O C ) )
21 20 ex 
 |-  ( ( A e. RR* /\ A W B ) -> ( w e. ( B P C ) -> w e. ( A O C ) ) )
22 21 ssrdv 
 |-  ( ( A e. RR* /\ A W B ) -> ( B P C ) C_ ( A O C ) )