Metamath Proof Explorer

Theorem btwnouttr2

Description: Outer transitivity law for betweenness. Left-hand side of Theorem 3.1 of Schwabhauser p. 30. (Contributed by Scott Fenton, 12-Jun-2013)

Ref Expression
Assertion btwnouttr2 
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) -> C Btwn <. A , D >. ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> N e. NN )
2 simp2l 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
3 simp3l 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
4 simp3r 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> D e. ( EE ` N ) )
5 axsegcon 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> E. x e. ( EE ` N ) ( C Btwn <. A , x >. /\ <. C , x >. Cgr <. C , D >. ) )
6 1 2 3 3 4 5 syl122anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> E. x e. ( EE ` N ) ( C Btwn <. A , x >. /\ <. C , x >. Cgr <. C , D >. ) )
7 6 adantr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) ) -> E. x e. ( EE ` N ) ( C Btwn <. A , x >. /\ <. C , x >. Cgr <. C , D >. ) )
8 simprrl 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) /\ ( C Btwn <. A , x >. /\ <. C , x >. Cgr <. C , D >. ) ) ) -> C Btwn <. A , x >. )
9 simprl1 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) /\ ( C Btwn <. A , x >. /\ <. C , x >. Cgr <. C , D >. ) ) ) -> B =/= C )
10 simpl2 
 |-  ( ( ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) /\ ( C Btwn <. A , x >. /\ <. C , x >. Cgr <. C , D >. ) ) -> B Btwn <. A , C >. )
11 simprl 
 |-  ( ( ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) /\ ( C Btwn <. A , x >. /\ <. C , x >. Cgr <. C , D >. ) ) -> C Btwn <. A , x >. )
12 10 11 jca 
 |-  ( ( ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) /\ ( C Btwn <. A , x >. /\ <. C , x >. Cgr <. C , D >. ) ) -> ( B Btwn <. A , C >. /\ C Btwn <. A , x >. ) )
13 12 adantl 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) /\ ( C Btwn <. A , x >. /\ <. C , x >. Cgr <. C , D >. ) ) ) -> ( B Btwn <. A , C >. /\ C Btwn <. A , x >. ) )
14 simpl1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> N e. NN )
15 simpl2l 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> A e. ( EE ` N ) )
16 simpl2r 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> B e. ( EE ` N ) )
17 simpl3l 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> C e. ( EE ` N ) )
18 simpr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> x e. ( EE ` N ) )
19 btwnexch3 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) -> ( ( B Btwn <. A , C >. /\ C Btwn <. A , x >. ) -> C Btwn <. B , x >. ) )
20 14 15 16 17 18 19 syl122anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( ( B Btwn <. A , C >. /\ C Btwn <. A , x >. ) -> C Btwn <. B , x >. ) )
21 20 adantr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) /\ ( C Btwn <. A , x >. /\ <. C , x >. Cgr <. C , D >. ) ) ) -> ( ( B Btwn <. A , C >. /\ C Btwn <. A , x >. ) -> C Btwn <. B , x >. ) )
22 13 21 mpd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) /\ ( C Btwn <. A , x >. /\ <. C , x >. Cgr <. C , D >. ) ) ) -> C Btwn <. B , x >. )
23 simprrr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) /\ ( C Btwn <. A , x >. /\ <. C , x >. Cgr <. C , D >. ) ) ) -> <. C , x >. Cgr <. C , D >. )
24 22 23 jca 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) /\ ( C Btwn <. A , x >. /\ <. C , x >. Cgr <. C , D >. ) ) ) -> ( C Btwn <. B , x >. /\ <. C , x >. Cgr <. C , D >. ) )
25 simprl3 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) /\ ( C Btwn <. A , x >. /\ <. C , x >. Cgr <. C , D >. ) ) ) -> C Btwn <. B , D >. )
26 simpl3r 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> D e. ( EE ` N ) )
27 14 17 26 cgrrflxd 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> <. C , D >. Cgr <. C , D >. )
28 27 adantr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) /\ ( C Btwn <. A , x >. /\ <. C , x >. Cgr <. C , D >. ) ) ) -> <. C , D >. Cgr <. C , D >. )
29 25 28 jca 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) /\ ( C Btwn <. A , x >. /\ <. C , x >. Cgr <. C , D >. ) ) ) -> ( C Btwn <. B , D >. /\ <. C , D >. Cgr <. C , D >. ) )
30 segconeq 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ x e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( B =/= C /\ ( C Btwn <. B , x >. /\ <. C , x >. Cgr <. C , D >. ) /\ ( C Btwn <. B , D >. /\ <. C , D >. Cgr <. C , D >. ) ) -> x = D ) )
31 14 17 17 26 16 18 26 30 syl133anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( ( B =/= C /\ ( C Btwn <. B , x >. /\ <. C , x >. Cgr <. C , D >. ) /\ ( C Btwn <. B , D >. /\ <. C , D >. Cgr <. C , D >. ) ) -> x = D ) )
32 31 adantr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) /\ ( C Btwn <. A , x >. /\ <. C , x >. Cgr <. C , D >. ) ) ) -> ( ( B =/= C /\ ( C Btwn <. B , x >. /\ <. C , x >. Cgr <. C , D >. ) /\ ( C Btwn <. B , D >. /\ <. C , D >. Cgr <. C , D >. ) ) -> x = D ) )
33 9 24 29 32 mp3and 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) /\ ( C Btwn <. A , x >. /\ <. C , x >. Cgr <. C , D >. ) ) ) -> x = D )
34 33 opeq2d 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) /\ ( C Btwn <. A , x >. /\ <. C , x >. Cgr <. C , D >. ) ) ) -> <. A , x >. = <. A , D >. )
35 8 34 breqtrd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) /\ ( C Btwn <. A , x >. /\ <. C , x >. Cgr <. C , D >. ) ) ) -> C Btwn <. A , D >. )
36 35 expr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) ) -> ( ( C Btwn <. A , x >. /\ <. C , x >. Cgr <. C , D >. ) -> C Btwn <. A , D >. ) )
37 36 an32s 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) ) /\ x e. ( EE ` N ) ) -> ( ( C Btwn <. A , x >. /\ <. C , x >. Cgr <. C , D >. ) -> C Btwn <. A , D >. ) )
38 37 rexlimdva 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) ) -> ( E. x e. ( EE ` N ) ( C Btwn <. A , x >. /\ <. C , x >. Cgr <. C , D >. ) -> C Btwn <. A , D >. ) )
39 7 38 mpd 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) ) -> C Btwn <. A , D >. )
40 39 ex 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) -> C Btwn <. A , D >. ) )