Metamath Proof Explorer

Theorem ixxssixx

Description: An interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007) (Revised by Mario Carneiro, 3-Nov-2013)

Ref Expression
Hypotheses ixx.1 
|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )
ixx.2 
|- P = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x T z /\ z U y ) } )
ixx.3 
|- ( ( A e. RR* /\ w e. RR* ) -> ( A R w -> A T w ) )
ixx.4 
|- ( ( w e. RR* /\ B e. RR* ) -> ( w S B -> w U B ) )
Assertion ixxssixx 
|- ( A O B ) C_ ( A P 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 ixx.2 
 |-  P = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x T z /\ z U y ) } )
3 ixx.3 
 |-  ( ( A e. RR* /\ w e. RR* ) -> ( A R w -> A T w ) )
4 ixx.4 
 |-  ( ( w e. RR* /\ B e. RR* ) -> ( w S B -> w U B ) )
5 1 elmpocl 
 |-  ( w e. ( A O B ) -> ( A e. RR* /\ B e. RR* ) )
6 simp1 
 |-  ( ( w e. RR* /\ A R w /\ w S B ) -> w e. RR* )
7 6 a1i 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( w e. RR* /\ A R w /\ w S B ) -> w e. RR* ) )
8 simpl 
 |-  ( ( A e. RR* /\ B e. RR* ) -> A e. RR* )
9 3simpa 
 |-  ( ( w e. RR* /\ A R w /\ w S B ) -> ( w e. RR* /\ A R w ) )
10 3 expimpd 
 |-  ( A e. RR* -> ( ( w e. RR* /\ A R w ) -> A T w ) )
11 8 9 10 syl2im 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( w e. RR* /\ A R w /\ w S B ) -> A T w ) )
12 simpr 
 |-  ( ( A e. RR* /\ B e. RR* ) -> B e. RR* )
13 3simpb 
 |-  ( ( w e. RR* /\ A R w /\ w S B ) -> ( w e. RR* /\ w S B ) )
14 4 ancoms 
 |-  ( ( B e. RR* /\ w e. RR* ) -> ( w S B -> w U B ) )
15 14 expimpd 
 |-  ( B e. RR* -> ( ( w e. RR* /\ w S B ) -> w U B ) )
16 12 13 15 syl2im 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( w e. RR* /\ A R w /\ w S B ) -> w U B ) )
17 7 11 16 3jcad 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( w e. RR* /\ A R w /\ w S B ) -> ( w e. RR* /\ A T w /\ w U B ) ) )
18 1 elixx1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( w e. ( A O B ) <-> ( w e. RR* /\ A R w /\ w S B ) ) )
19 2 elixx1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( w e. ( A P B ) <-> ( w e. RR* /\ A T w /\ w U B ) ) )
20 17 18 19 3imtr4d 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( w e. ( A O B ) -> w e. ( A P B ) ) )
21 5 20 mpcom 
 |-  ( w e. ( A O B ) -> w e. ( A P B ) )
22 21 ssriv 
 |-  ( A O B ) C_ ( A P B )