Metamath Proof Explorer

Theorem btwnswapid

Description: If you can swap the first two arguments of a betweenness statement, then those arguments are identical. Theorem 3.4 of Schwabhauser p. 30. (Contributed by Scott Fenton, 12-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> N e. NN )
2 simpr2 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
3 simpr1 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
4 simpr3 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
5 axpasch 
 |-  ( ( N e. NN /\ ( B e. ( EE ` N ) /\ A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( ( A Btwn <. B , C >. /\ B Btwn <. A , C >. ) -> E. x e. ( EE ` N ) ( x Btwn <. A , A >. /\ x Btwn <. B , B >. ) ) )
6 1 2 3 4 3 2 5 syl132anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( A Btwn <. B , C >. /\ B Btwn <. A , C >. ) -> E. x e. ( EE ` N ) ( x Btwn <. A , A >. /\ x Btwn <. B , B >. ) ) )
7 simpll 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> N e. NN )
8 simpr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> x e. ( EE ` N ) )
9 simplr1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> A e. ( EE ` N ) )
10 axbtwnid 
 |-  ( ( N e. NN /\ x e. ( EE ` N ) /\ A e. ( EE ` N ) ) -> ( x Btwn <. A , A >. -> x = A ) )
11 7 8 9 10 syl3anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( x Btwn <. A , A >. -> x = A ) )
12 simplr2 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> B e. ( EE ` N ) )
13 axbtwnid 
 |-  ( ( N e. NN /\ x e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( x Btwn <. B , B >. -> x = B ) )
14 7 8 12 13 syl3anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( x Btwn <. B , B >. -> x = B ) )
15 11 14 anim12d 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( ( x Btwn <. A , A >. /\ x Btwn <. B , B >. ) -> ( x = A /\ x = B ) ) )
16 eqtr2 
 |-  ( ( x = A /\ x = B ) -> A = B )
17 15 16 syl6 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( ( x Btwn <. A , A >. /\ x Btwn <. B , B >. ) -> A = B ) )
18 17 rexlimdva 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( E. x e. ( EE ` N ) ( x Btwn <. A , A >. /\ x Btwn <. B , B >. ) -> A = B ) )
19 6 18 syld 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( A Btwn <. B , C >. /\ B Btwn <. A , C >. ) -> A = B ) )