Metamath Proof Explorer

Theorem ixxdisj

Description: Split an interval into disjoint pieces. (Contributed by Mario Carneiro, 16-Jun-2014)

Ref Expression
Hypotheses ixx.1 
|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )
ixxun.2 
|- P = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x T z /\ z U y ) } )
ixxun.3 
|- ( ( B e. RR* /\ w e. RR* ) -> ( B T w <-> -. w S B ) )
Assertion ixxdisj 
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A O B ) i^i ( B P 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 ixxun.2 
 |-  P = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x T z /\ z U y ) } )
3 ixxun.3 
 |-  ( ( B e. RR* /\ w e. RR* ) -> ( B T w <-> -. w S B ) )
4 elin 
 |-  ( w e. ( ( A O B ) i^i ( B P C ) ) <-> ( w e. ( A O B ) /\ w e. ( B P C ) ) )
5 1 elixx1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( w e. ( A O B ) <-> ( w e. RR* /\ A R w /\ w S B ) ) )
6 5 3adant3 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( w e. ( A O B ) <-> ( w e. RR* /\ A R w /\ w S B ) ) )
7 6 biimpa 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ w e. ( A O B ) ) -> ( w e. RR* /\ A R w /\ w S B ) )
8 7 simp3d 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ w e. ( A O B ) ) -> w S B )
9 8 adantrr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( w e. ( A O B ) /\ w e. ( B P C ) ) ) -> w S B )
10 2 elixx1 
 |-  ( ( B e. RR* /\ C e. RR* ) -> ( w e. ( B P C ) <-> ( w e. RR* /\ B T w /\ w U C ) ) )
11 10 3adant1 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( w e. ( B P C ) <-> ( w e. RR* /\ B T w /\ w U C ) ) )
12 11 biimpa 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ w e. ( B P C ) ) -> ( w e. RR* /\ B T w /\ w U C ) )
13 12 simp2d 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ w e. ( B P C ) ) -> B T w )
14 simpl2 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ w e. ( B P C ) ) -> B e. RR* )
15 12 simp1d 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ w e. ( B P C ) ) -> w e. RR* )
16 14 15 3 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ w e. ( B P C ) ) -> ( B T w <-> -. w S B ) )
17 13 16 mpbid 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ w e. ( B P C ) ) -> -. w S B )
18 17 adantrl 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( w e. ( A O B ) /\ w e. ( B P C ) ) ) -> -. w S B )
19 9 18 pm2.65da 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> -. ( w e. ( A O B ) /\ w e. ( B P C ) ) )
20 19 pm2.21d 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( w e. ( A O B ) /\ w e. ( B P C ) ) -> w e. (/) ) )
21 4 20 syl5bi 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( w e. ( ( A O B ) i^i ( B P C ) ) -> w e. (/) ) )
22 21 ssrdv 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A O B ) i^i ( B P C ) ) C_ (/) )
23 ss0 
 |-  ( ( ( A O B ) i^i ( B P C ) ) C_ (/) -> ( ( A O B ) i^i ( B P C ) ) = (/) )
24 22 23 syl 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A O B ) i^i ( B P C ) ) = (/) )