Metamath Proof Explorer

Theorem ixxun

Description: Split an interval into two parts. (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 ) )
ixxun.4 
|- Q = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z U y ) } )
ixxun.5 
|- ( ( w e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( w S B /\ B X C ) -> w U C ) )
ixxun.6 
|- ( ( A e. RR* /\ B e. RR* /\ w e. RR* ) -> ( ( A W B /\ B T w ) -> A R w ) )
Assertion ixxun 
|- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) -> ( ( A O B ) u. ( B P C ) ) = ( A Q 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 ixxun.4 
 |-  Q = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z U y ) } )
5 ixxun.5 
 |-  ( ( w e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( w S B /\ B X C ) -> w U C ) )
6 ixxun.6 
 |-  ( ( A e. RR* /\ B e. RR* /\ w e. RR* ) -> ( ( A W B /\ B T w ) -> A R w ) )
7 elun 
 |-  ( w e. ( ( A O B ) u. ( B P C ) ) <-> ( w e. ( A O B ) \/ w e. ( B P C ) ) )
8 simpl1 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) -> A e. RR* )
9 simpl2 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) -> B e. RR* )
10 1 elixx1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( w e. ( A O B ) <-> ( w e. RR* /\ A R w /\ w S B ) ) )
11 8 9 10 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) -> ( w e. ( A O B ) <-> ( w e. RR* /\ A R w /\ w S B ) ) )
12 11 biimpa 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( A O B ) ) -> ( w e. RR* /\ A R w /\ w S B ) )
13 12 simp1d 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( A O B ) ) -> w e. RR* )
14 12 simp2d 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( A O B ) ) -> A R w )
15 12 simp3d 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( A O B ) ) -> w S B )
16 simplrr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( A O B ) ) -> B X C )
17 9 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( A O B ) ) -> B e. RR* )
18 simpl3 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) -> C e. RR* )
19 18 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( A O B ) ) -> C e. RR* )
20 13 17 19 5 syl3anc 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( A O B ) ) -> ( ( w S B /\ B X C ) -> w U C ) )
21 15 16 20 mp2and 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( A O B ) ) -> w U C )
22 13 14 21 3jca 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( A O B ) ) -> ( w e. RR* /\ A R w /\ w U C ) )
23 2 elixx1 
 |-  ( ( B e. RR* /\ C e. RR* ) -> ( w e. ( B P C ) <-> ( w e. RR* /\ B T w /\ w U C ) ) )
24 9 18 23 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) -> ( w e. ( B P C ) <-> ( w e. RR* /\ B T w /\ w U C ) ) )
25 24 biimpa 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( B P C ) ) -> ( w e. RR* /\ B T w /\ w U C ) )
26 25 simp1d 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( B P C ) ) -> w e. RR* )
27 simplrl 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( B P C ) ) -> A W B )
28 25 simp2d 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( B P C ) ) -> B T w )
29 8 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( B P C ) ) -> A e. RR* )
30 9 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( B P C ) ) -> B e. RR* )
31 29 30 26 6 syl3anc 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( B P C ) ) -> ( ( A W B /\ B T w ) -> A R w ) )
32 27 28 31 mp2and 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( B P C ) ) -> A R w )
33 25 simp3d 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( B P C ) ) -> w U C )
34 26 32 33 3jca 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( B P C ) ) -> ( w e. RR* /\ A R w /\ w U C ) )
35 22 34 jaodan 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ ( w e. ( A O B ) \/ w e. ( B P C ) ) ) -> ( w e. RR* /\ A R w /\ w U C ) )
36 4 elixx1 
 |-  ( ( A e. RR* /\ C e. RR* ) -> ( w e. ( A Q C ) <-> ( w e. RR* /\ A R w /\ w U C ) ) )
37 8 18 36 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) -> ( w e. ( A Q C ) <-> ( w e. RR* /\ A R w /\ w U C ) ) )
38 37 biimpar 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ ( w e. RR* /\ A R w /\ w U C ) ) -> w e. ( A Q C ) )
39 35 38 syldan 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ ( w e. ( A O B ) \/ w e. ( B P C ) ) ) -> w e. ( A Q C ) )
40 exmid 
 |-  ( w S B \/ -. w S B )
41 37 biimpa 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( A Q C ) ) -> ( w e. RR* /\ A R w /\ w U C ) )
42 41 simp1d 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( A Q C ) ) -> w e. RR* )
43 41 simp2d 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( A Q C ) ) -> A R w )
44 42 43 jca 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( A Q C ) ) -> ( w e. RR* /\ A R w ) )
45 df-3an 
 |-  ( ( w e. RR* /\ A R w /\ w S B ) <-> ( ( w e. RR* /\ A R w ) /\ w S B ) )
46 11 45 bitrdi 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) -> ( w e. ( A O B ) <-> ( ( w e. RR* /\ A R w ) /\ w S B ) ) )
47 46 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( A Q C ) ) -> ( w e. ( A O B ) <-> ( ( w e. RR* /\ A R w ) /\ w S B ) ) )
48 44 47 mpbirand 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( A Q C ) ) -> ( w e. ( A O B ) <-> w S B ) )
49 3anan12 
 |-  ( ( w e. RR* /\ B T w /\ w U C ) <-> ( B T w /\ ( w e. RR* /\ w U C ) ) )
50 24 49 bitrdi 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) -> ( w e. ( B P C ) <-> ( B T w /\ ( w e. RR* /\ w U C ) ) ) )
51 50 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( A Q C ) ) -> ( w e. ( B P C ) <-> ( B T w /\ ( w e. RR* /\ w U C ) ) ) )
52 41 simp3d 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( A Q C ) ) -> w U C )
53 42 52 jca 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( A Q C ) ) -> ( w e. RR* /\ w U C ) )
54 53 biantrud 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( A Q C ) ) -> ( B T w <-> ( B T w /\ ( w e. RR* /\ w U C ) ) ) )
55 9 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( A Q C ) ) -> B e. RR* )
56 55 42 3 syl2anc 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( A Q C ) ) -> ( B T w <-> -. w S B ) )
57 51 54 56 3bitr2d 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( A Q C ) ) -> ( w e. ( B P C ) <-> -. w S B ) )
58 48 57 orbi12d 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( A Q C ) ) -> ( ( w e. ( A O B ) \/ w e. ( B P C ) ) <-> ( w S B \/ -. w S B ) ) )
59 40 58 mpbiri 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) /\ w e. ( A Q C ) ) -> ( w e. ( A O B ) \/ w e. ( B P C ) ) )
60 39 59 impbida 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) -> ( ( w e. ( A O B ) \/ w e. ( B P C ) ) <-> w e. ( A Q C ) ) )
61 7 60 syl5bb 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) -> ( w e. ( ( A O B ) u. ( B P C ) ) <-> w e. ( A Q C ) ) )
62 61 eqrdv 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A W B /\ B X C ) ) -> ( ( A O B ) u. ( B P C ) ) = ( A Q C ) )