MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axtgbtwnid Structured version   Unicode version

Theorem axtgbtwnid 24377
Description: Identity of Betweenness. Axiom A6 of [Schwabhauser] p. 11. (Contributed by Thierry Arnoux, 15-Mar-2019.)
Hypotheses
Ref Expression
axtrkg.p  |-  P  =  ( Base `  G
)
axtrkg.d  |-  .-  =  ( dist `  G )
axtrkg.i  |-  I  =  (Itv `  G )
axtrkg.g  |-  ( ph  ->  G  e. TarskiG )
axtgbtwnid.1  |-  ( ph  ->  X  e.  P )
axtgbtwnid.2  |-  ( ph  ->  Y  e.  P )
axtgbtwnid.3  |-  ( ph  ->  Y  e.  ( X I X ) )
Assertion
Ref Expression
axtgbtwnid  |-  ( ph  ->  X  =  Y )

Proof of Theorem axtgbtwnid
Dummy variables  f 
i  p  x  y  z  a  b  v  s  t  u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-trkg 24364 . . . . 5  |- TarskiG  =  ( (TarskiGC  i^i TarskiGB )  i^i  (TarskiGCB  i^i  {
f  |  [. ( Base `  f )  /  p ]. [. (Itv `  f )  /  i ]. (LineG `  f )  =  ( x  e.  p ,  y  e.  ( p  \  {
x } )  |->  { z  e.  p  |  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) } ) } ) )
2 inss1 3688 . . . . . 6  |-  ( (TarskiGC  i^i TarskiGB )  i^i  (TarskiGCB  i^i  { f  | 
[. ( Base `  f
)  /  p ]. [. (Itv `  f )  /  i ]. (LineG `  f )  =  ( x  e.  p ,  y  e.  ( p 
\  { x }
)  |->  { z  e.  p  |  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) } ) } ) )  C_  (TarskiGC  i^i TarskiGB )
3 inss2 3689 . . . . . 6  |-  (TarskiGC  i^i TarskiGB )  C_ TarskiGB
42, 3sstri 3479 . . . . 5  |-  ( (TarskiGC  i^i TarskiGB )  i^i  (TarskiGCB  i^i  { f  | 
[. ( Base `  f
)  /  p ]. [. (Itv `  f )  /  i ]. (LineG `  f )  =  ( x  e.  p ,  y  e.  ( p 
\  { x }
)  |->  { z  e.  p  |  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) } ) } ) )  C_ TarskiGB
51, 4eqsstri 3500 . . . 4  |- TarskiG  C_ TarskiGB
6 axtrkg.g . . . 4  |-  ( ph  ->  G  e. TarskiG )
75, 6sseldi 3468 . . 3  |-  ( ph  ->  G  e. TarskiGB )
8 axtrkg.p . . . . . 6  |-  P  =  ( Base `  G
)
9 axtrkg.d . . . . . 6  |-  .-  =  ( dist `  G )
10 axtrkg.i . . . . . 6  |-  I  =  (Itv `  G )
118, 9, 10istrkgb 24366 . . . . 5  |-  ( G  e. TarskiGB  <->  ( G  e.  _V  /\  ( A. x  e.  P  A. y  e.  P  ( y  e.  ( x I x )  ->  x  =  y )  /\  A. x  e.  P  A. y  e.  P  A. z  e.  P  A. u  e.  P  A. v  e.  P  ( (
u  e.  ( x I z )  /\  v  e.  ( y
I z ) )  ->  E. a  e.  P  ( a  e.  ( u I y )  /\  a  e.  ( v I x ) ) )  /\  A. s  e.  ~P  P A. t  e.  ~P  P ( E. a  e.  P  A. x  e.  s  A. y  e.  t  x  e.  ( a I y )  ->  E. b  e.  P  A. x  e.  s  A. y  e.  t  b  e.  ( x I y ) ) ) ) )
1211simprbi 465 . . . 4  |-  ( G  e. TarskiGB 
->  ( A. x  e.  P  A. y  e.  P  ( y  e.  ( x I x )  ->  x  =  y )  /\  A. x  e.  P  A. y  e.  P  A. z  e.  P  A. u  e.  P  A. v  e.  P  (
( u  e.  ( x I z )  /\  v  e.  ( y I z ) )  ->  E. a  e.  P  ( a  e.  ( u I y )  /\  a  e.  ( v I x ) ) )  /\  A. s  e.  ~P  P A. t  e.  ~P  P ( E. a  e.  P  A. x  e.  s  A. y  e.  t  x  e.  ( a I y )  ->  E. b  e.  P  A. x  e.  s  A. y  e.  t  b  e.  ( x I y ) ) ) )
1312simp1d 1017 . . 3  |-  ( G  e. TarskiGB 
->  A. x  e.  P  A. y  e.  P  ( y  e.  ( x I x )  ->  x  =  y ) )
147, 13syl 17 . 2  |-  ( ph  ->  A. x  e.  P  A. y  e.  P  ( y  e.  ( x I x )  ->  x  =  y ) )
15 axtgbtwnid.3 . 2  |-  ( ph  ->  Y  e.  ( X I X ) )
16 axtgbtwnid.1 . . 3  |-  ( ph  ->  X  e.  P )
17 axtgbtwnid.2 . . 3  |-  ( ph  ->  Y  e.  P )
18 id 23 . . . . . . 7  |-  ( x  =  X  ->  x  =  X )
1918, 18oveq12d 6323 . . . . . 6  |-  ( x  =  X  ->  (
x I x )  =  ( X I X ) )
2019eleq2d 2499 . . . . 5  |-  ( x  =  X  ->  (
y  e.  ( x I x )  <->  y  e.  ( X I X ) ) )
21 eqeq1 2433 . . . . 5  |-  ( x  =  X  ->  (
x  =  y  <->  X  =  y ) )
2220, 21imbi12d 321 . . . 4  |-  ( x  =  X  ->  (
( y  e.  ( x I x )  ->  x  =  y )  <->  ( y  e.  ( X I X )  ->  X  =  y ) ) )
23 eleq1 2501 . . . . 5  |-  ( y  =  Y  ->  (
y  e.  ( X I X )  <->  Y  e.  ( X I X ) ) )
24 eqeq2 2444 . . . . 5  |-  ( y  =  Y  ->  ( X  =  y  <->  X  =  Y ) )
2523, 24imbi12d 321 . . . 4  |-  ( y  =  Y  ->  (
( y  e.  ( X I X )  ->  X  =  y )  <->  ( Y  e.  ( X I X )  ->  X  =  Y ) ) )
2622, 25rspc2v 3197 . . 3  |-  ( ( X  e.  P  /\  Y  e.  P )  ->  ( A. x  e.  P  A. y  e.  P  ( y  e.  ( x I x )  ->  x  =  y )  ->  ( Y  e.  ( X I X )  ->  X  =  Y ) ) )
2716, 17, 26syl2anc 665 . 2  |-  ( ph  ->  ( A. x  e.  P  A. y  e.  P  ( y  e.  ( x I x )  ->  x  =  y )  ->  ( Y  e.  ( X I X )  ->  X  =  Y ) ) )
2814, 15, 27mp2d 46 1  |-  ( ph  ->  X  =  Y )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    \/ w3o 981    /\ w3a 982    = wceq 1437    e. wcel 1870   {cab 2414   A.wral 2782   E.wrex 2783   {crab 2786   _Vcvv 3087   [.wsbc 3305    \ cdif 3439    i^i cin 3441   ~Pcpw 3985   {csn 4002   ` cfv 5601  (class class class)co 6305    |-> cmpt2 6307   Basecbs 15084   distcds 15161  TarskiGcstrkg 24341  TarskiGCcstrkgc 24342  TarskiGBcstrkgb 24343  TarskiGCBcstrkgcb 24344  Itvcitv 24347  LineGclng 24348
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-nul 4556
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-sbc 3306  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-iota 5565  df-fv 5609  df-ov 6308  df-trkgb 24360  df-trkg 24364
This theorem is referenced by:  tgbtwncom  24395  tgbtwnne  24397  tgbtwnswapid  24399  tgbtwnintr  24400  tgifscgr  24416  tgidinside  24476  tgbtwnconn1lem3  24479  coltr3  24553  mirinv  24571  miriso  24574  krippenlem  24592  midexlem  24594  colperpexlem3  24631  oppne3  24642  oppnid  24645  opphllem1  24646  midid  24679  lmiisolem  24694  f1otrg  24747
  Copyright terms: Public domain W3C validator