Metamath Proof Explorer

Theorem btwntriv2

Description: Betweenness always holds for the second endpoint. Theorem 3.1 of Schwabhauser p. 30. (Contributed by Scott Fenton, 12-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> N e. NN )
2 simp2 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> A e. ( EE ` N ) )
3 simp3 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> B e. ( EE ` N ) )
4 axsegcon 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> E. x e. ( EE ` N ) ( B Btwn <. A , x >. /\ <. B , x >. Cgr <. B , B >. ) )
5 1 2 3 3 3 4 syl122anc 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> E. x e. ( EE ` N ) ( B Btwn <. A , x >. /\ <. B , x >. Cgr <. B , B >. ) )
6 simpl1 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ x e. ( EE ` N ) ) -> N e. NN )
7 simpl3 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ x e. ( EE ` N ) ) -> B e. ( EE ` N ) )
8 simpr 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ x e. ( EE ` N ) ) -> x e. ( EE ` N ) )
9 axcgrid 
 |-  ( ( N e. NN /\ ( B e. ( EE ` N ) /\ x e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( <. B , x >. Cgr <. B , B >. -> B = x ) )
10 6 7 8 7 9 syl13anc 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ x e. ( EE ` N ) ) -> ( <. B , x >. Cgr <. B , B >. -> B = x ) )
11 opeq2 
 |-  ( B = x -> <. A , B >. = <. A , x >. )
12 11 breq2d 
 |-  ( B = x -> ( B Btwn <. A , B >. <-> B Btwn <. A , x >. ) )
13 12 biimprd 
 |-  ( B = x -> ( B Btwn <. A , x >. -> B Btwn <. A , B >. ) )
14 10 13 syl6 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ x e. ( EE ` N ) ) -> ( <. B , x >. Cgr <. B , B >. -> ( B Btwn <. A , x >. -> B Btwn <. A , B >. ) ) )
15 14 impd 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ x e. ( EE ` N ) ) -> ( ( <. B , x >. Cgr <. B , B >. /\ B Btwn <. A , x >. ) -> B Btwn <. A , B >. ) )
16 15 ancomsd 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ x e. ( EE ` N ) ) -> ( ( B Btwn <. A , x >. /\ <. B , x >. Cgr <. B , B >. ) -> B Btwn <. A , B >. ) )
17 16 rexlimdva 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( E. x e. ( EE ` N ) ( B Btwn <. A , x >. /\ <. B , x >. Cgr <. B , B >. ) -> B Btwn <. A , B >. ) )
18 5 17 mpd 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> B Btwn <. A , B >. )