This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ixxss2

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