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

Theorem axtgbtwnid 22949
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 22938 . . . . 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 3591 . . . . . 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 3592 . . . . . 6  |-  (TarskiGC  i^i TarskiGB )  C_ TarskiGB
42, 3sstri 3386 . . . . 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 3407 . . . 4  |- TarskiG  C_ TarskiGB
6 axtrkg.g . . . 4  |-  ( ph  ->  G  e. TarskiG )
75, 6sseldi 3375 . . 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 22940 . . . . 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 464 . . . 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 1000 . . 3  |-  ( G  e. TarskiGB 
->  A. x  e.  P  A. y  e.  P  ( y  e.  ( x I x )  ->  x  =  y ) )
147, 13syl 16 . 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 22 . . . . . . 7  |-  ( x  =  X  ->  x  =  X )
1918, 18oveq12d 6130 . . . . . 6  |-  ( x  =  X  ->  (
x I x )  =  ( X I X ) )
2019eleq2d 2510 . . . . 5  |-  ( x  =  X  ->  (
y  e.  ( x I x )  <->  y  e.  ( X I X ) ) )
21 eqeq1 2449 . . . . 5  |-  ( x  =  X  ->  (
x  =  y  <->  X  =  y ) )
2220, 21imbi12d 320 . . . 4  |-  ( x  =  X  ->  (
( y  e.  ( x I x )  ->  x  =  y )  <->  ( y  e.  ( X I X )  ->  X  =  y ) ) )
23 eleq1 2503 . . . . 5  |-  ( y  =  Y  ->  (
y  e.  ( X I X )  <->  Y  e.  ( X I X ) ) )
24 eqeq2 2452 . . . . 5  |-  ( y  =  Y  ->  ( X  =  y  <->  X  =  Y ) )
2523, 24imbi12d 320 . . . 4  |-  ( y  =  Y  ->  (
( y  e.  ( X I X )  ->  X  =  y )  <->  ( Y  e.  ( X I X )  ->  X  =  Y ) ) )
2622, 25rspc2v 3100 . . 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 661 . 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 45 1  |-  ( ph  ->  X  =  Y )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    \/ w3o 964    /\ w3a 965    = wceq 1369    e. wcel 1756   {cab 2429   A.wral 2736   E.wrex 2737   {crab 2740   _Vcvv 2993   [.wsbc 3207    \ cdif 3346    i^i cin 3348   ~Pcpw 3881   {csn 3898   ` cfv 5439  (class class class)co 6112    e. cmpt2 6114   Basecbs 14195   distcds 14268  TarskiGcstrkg 22911  TarskiGCcstrkgc 22912  TarskiGBcstrkgb 22913  TarskiGCBcstrkgcb 22914  Itvcitv 22919  LineGclng 22920
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-nul 4442
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-sbc 3208  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-op 3905  df-uni 4113  df-br 4314  df-iota 5402  df-fv 5447  df-ov 6115  df-trkgb 22932  df-trkg 22938
This theorem is referenced by:  tgbtwncom  22964  tgbtwnswapid  22967  tgbtwnintr  22968  tgifscgr  22983  tgidinside  23025  tgbtwnconn1lem3  23028  mirinv  23092  miriso  23095  krippenlem  23106  midexlem  23108  f1otrg  23139
  Copyright terms: Public domain W3C validator