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

Theorem axtgpasch 22928
Description: Axiom of Pasch, Axiom A7 of [Schwabhauser] p. 12. (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 )
axtgpasch.1  |-  ( ph  ->  X  e.  P )
axtgpasch.2  |-  ( ph  ->  Y  e.  P )
axtgpasch.3  |-  ( ph  ->  Z  e.  P )
axtgpasch.4  |-  ( ph  ->  U  e.  P )
axtgpasch.5  |-  ( ph  ->  V  e.  P )
axtgpasch.6  |-  ( ph  ->  U  e.  ( X I Z ) )
axtgpasch.7  |-  ( ph  ->  V  e.  ( Y I Z ) )
Assertion
Ref Expression
axtgpasch  |-  ( ph  ->  E. a  e.  P  ( a  e.  ( U I Y )  /\  a  e.  ( V I X ) ) )
Distinct variable groups:    I, a    P, a    U, a    X, a    Y, a    Z, a    V, a    .- , a
Allowed substitution hints:    ph( a)    G( a)

Proof of Theorem axtgpasch
Dummy variables  f 
i  p  x  y  z  b  v  s  t  u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 axtgpasch.6 . 2  |-  ( ph  ->  U  e.  ( X I Z ) )
2 axtgpasch.7 . 2  |-  ( ph  ->  V  e.  ( Y I Z ) )
3 df-trkg 22916 . . . . . . 7  |- 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 ) ) } ) } ) )
4 inss1 3570 . . . . . . . 8  |-  ( (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 )
5 inss2 3571 . . . . . . . 8  |-  (TarskiGC  i^i TarskiGB )  C_ TarskiGB
64, 5sstri 3365 . . . . . . 7  |-  ( (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
73, 6eqsstri 3386 . . . . . 6  |- TarskiG  C_ TarskiGB
8 axtrkg.g . . . . . 6  |-  ( ph  ->  G  e. TarskiG )
97, 8sseldi 3354 . . . . 5  |-  ( ph  ->  G  e. TarskiGB )
10 axtrkg.p . . . . . . . 8  |-  P  =  ( Base `  G
)
11 axtrkg.d . . . . . . . 8  |-  .-  =  ( dist `  G )
12 axtrkg.i . . . . . . . 8  |-  I  =  (Itv `  G )
1310, 11, 12istrkgb 22918 . . . . . . 7  |-  ( 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 ) ) ) ) )
1413simprbi 464 . . . . . 6  |-  ( 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 ) ) ) )
1514simp2d 1001 . . . . 5  |-  ( G  e. TarskiGB 
->  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 ) ) ) )
169, 15syl 16 . . . 4  |-  ( ph  ->  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 ) ) ) )
17 axtgpasch.1 . . . . 5  |-  ( ph  ->  X  e.  P )
18 axtgpasch.2 . . . . 5  |-  ( ph  ->  Y  e.  P )
19 axtgpasch.3 . . . . 5  |-  ( ph  ->  Z  e.  P )
20 oveq1 6098 . . . . . . . . . 10  |-  ( x  =  X  ->  (
x I z )  =  ( X I z ) )
2120eleq2d 2510 . . . . . . . . 9  |-  ( x  =  X  ->  (
u  e.  ( x I z )  <->  u  e.  ( X I z ) ) )
2221anbi1d 704 . . . . . . . 8  |-  ( x  =  X  ->  (
( u  e.  ( x I z )  /\  v  e.  ( y I z ) )  <->  ( u  e.  ( X I z )  /\  v  e.  ( y I z ) ) ) )
23 oveq2 6099 . . . . . . . . . . 11  |-  ( x  =  X  ->  (
v I x )  =  ( v I X ) )
2423eleq2d 2510 . . . . . . . . . 10  |-  ( x  =  X  ->  (
a  e.  ( v I x )  <->  a  e.  ( v I X ) ) )
2524anbi2d 703 . . . . . . . . 9  |-  ( x  =  X  ->  (
( a  e.  ( u I y )  /\  a  e.  ( v I x ) )  <->  ( a  e.  ( u I y )  /\  a  e.  ( v I X ) ) ) )
2625rexbidv 2736 . . . . . . . 8  |-  ( x  =  X  ->  ( E. a  e.  P  ( a  e.  ( u I y )  /\  a  e.  ( v I x ) )  <->  E. a  e.  P  ( a  e.  ( u I y )  /\  a  e.  ( v I X ) ) ) )
2722, 26imbi12d 320 . . . . . . 7  |-  ( x  =  X  ->  (
( ( u  e.  ( x I z )  /\  v  e.  ( y I z ) )  ->  E. a  e.  P  ( a  e.  ( u I y )  /\  a  e.  ( v I x ) ) )  <->  ( (
u  e.  ( X I z )  /\  v  e.  ( y
I z ) )  ->  E. a  e.  P  ( a  e.  ( u I y )  /\  a  e.  ( v I X ) ) ) ) )
28272ralbidv 2757 . . . . . 6  |-  ( x  =  X  ->  ( 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. 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 ) ) ) ) )
29 oveq1 6098 . . . . . . . . . 10  |-  ( y  =  Y  ->  (
y I z )  =  ( Y I z ) )
3029eleq2d 2510 . . . . . . . . 9  |-  ( y  =  Y  ->  (
v  e.  ( y I z )  <->  v  e.  ( Y I z ) ) )
3130anbi2d 703 . . . . . . . 8  |-  ( y  =  Y  ->  (
( u  e.  ( X I z )  /\  v  e.  ( y I z ) )  <->  ( u  e.  ( X I z )  /\  v  e.  ( Y I z ) ) ) )
32 oveq2 6099 . . . . . . . . . . 11  |-  ( y  =  Y  ->  (
u I y )  =  ( u I Y ) )
3332eleq2d 2510 . . . . . . . . . 10  |-  ( y  =  Y  ->  (
a  e.  ( u I y )  <->  a  e.  ( u I Y ) ) )
3433anbi1d 704 . . . . . . . . 9  |-  ( y  =  Y  ->  (
( a  e.  ( u I y )  /\  a  e.  ( v I X ) )  <->  ( a  e.  ( u I Y )  /\  a  e.  ( v I X ) ) ) )
3534rexbidv 2736 . . . . . . . 8  |-  ( y  =  Y  ->  ( E. a  e.  P  ( a  e.  ( u I y )  /\  a  e.  ( v I X ) )  <->  E. a  e.  P  ( a  e.  ( u I Y )  /\  a  e.  ( v I X ) ) ) )
3631, 35imbi12d 320 . . . . . . 7  |-  ( y  =  Y  ->  (
( ( u  e.  ( X I z )  /\  v  e.  ( y I z ) )  ->  E. a  e.  P  ( a  e.  ( u I y )  /\  a  e.  ( v I X ) ) )  <->  ( (
u  e.  ( X I z )  /\  v  e.  ( Y I z ) )  ->  E. a  e.  P  ( a  e.  ( u I Y )  /\  a  e.  ( v I X ) ) ) ) )
37362ralbidv 2757 . . . . . 6  |-  ( y  =  Y  ->  ( 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. 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 ) ) ) ) )
38 oveq2 6099 . . . . . . . . . 10  |-  ( z  =  Z  ->  ( X I z )  =  ( X I Z ) )
3938eleq2d 2510 . . . . . . . . 9  |-  ( z  =  Z  ->  (
u  e.  ( X I z )  <->  u  e.  ( X I Z ) ) )
40 oveq2 6099 . . . . . . . . . 10  |-  ( z  =  Z  ->  ( Y I z )  =  ( Y I Z ) )
4140eleq2d 2510 . . . . . . . . 9  |-  ( z  =  Z  ->  (
v  e.  ( Y I z )  <->  v  e.  ( Y I Z ) ) )
4239, 41anbi12d 710 . . . . . . . 8  |-  ( z  =  Z  ->  (
( u  e.  ( X I z )  /\  v  e.  ( Y I z ) )  <->  ( u  e.  ( X I Z )  /\  v  e.  ( Y I Z ) ) ) )
4342imbi1d 317 . . . . . . 7  |-  ( z  =  Z  ->  (
( ( u  e.  ( X I z )  /\  v  e.  ( Y I z ) )  ->  E. a  e.  P  ( a  e.  ( u I Y )  /\  a  e.  ( v I X ) ) )  <->  ( (
u  e.  ( X I Z )  /\  v  e.  ( Y I Z ) )  ->  E. a  e.  P  ( a  e.  ( u I Y )  /\  a  e.  ( v I X ) ) ) ) )
44432ralbidv 2757 . . . . . 6  |-  ( z  =  Z  ->  ( 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. 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 ) ) ) ) )
4528, 37, 44rspc3v 3082 . . . . 5  |-  ( ( X  e.  P  /\  Y  e.  P  /\  Z  e.  P )  ->  ( 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. 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 ) ) ) ) )
4617, 18, 19, 45syl3anc 1218 . . . 4  |-  ( ph  ->  ( 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. 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 ) ) ) ) )
4716, 46mpd 15 . . 3  |-  ( ph  ->  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 ) ) ) )
48 axtgpasch.4 . . . 4  |-  ( ph  ->  U  e.  P )
49 axtgpasch.5 . . . 4  |-  ( ph  ->  V  e.  P )
50 eleq1 2503 . . . . . . 7  |-  ( u  =  U  ->  (
u  e.  ( X I Z )  <->  U  e.  ( X I Z ) ) )
5150anbi1d 704 . . . . . 6  |-  ( u  =  U  ->  (
( u  e.  ( X I Z )  /\  v  e.  ( Y I Z ) )  <->  ( U  e.  ( X I Z )  /\  v  e.  ( Y I Z ) ) ) )
52 oveq1 6098 . . . . . . . . 9  |-  ( u  =  U  ->  (
u I Y )  =  ( U I Y ) )
5352eleq2d 2510 . . . . . . . 8  |-  ( u  =  U  ->  (
a  e.  ( u I Y )  <->  a  e.  ( U I Y ) ) )
5453anbi1d 704 . . . . . . 7  |-  ( u  =  U  ->  (
( a  e.  ( u I Y )  /\  a  e.  ( v I X ) )  <->  ( a  e.  ( U I Y )  /\  a  e.  ( v I X ) ) ) )
5554rexbidv 2736 . . . . . 6  |-  ( u  =  U  ->  ( E. a  e.  P  ( a  e.  ( u I Y )  /\  a  e.  ( v I X ) )  <->  E. a  e.  P  ( a  e.  ( U I Y )  /\  a  e.  ( v I X ) ) ) )
5651, 55imbi12d 320 . . . . 5  |-  ( u  =  U  ->  (
( ( u  e.  ( X I Z )  /\  v  e.  ( Y I Z ) )  ->  E. a  e.  P  ( a  e.  ( u I Y )  /\  a  e.  ( v I X ) ) )  <->  ( ( U  e.  ( X I Z )  /\  v  e.  ( Y I Z ) )  ->  E. a  e.  P  ( a  e.  ( U I Y )  /\  a  e.  ( v I X ) ) ) ) )
57 eleq1 2503 . . . . . . 7  |-  ( v  =  V  ->  (
v  e.  ( Y I Z )  <->  V  e.  ( Y I Z ) ) )
5857anbi2d 703 . . . . . 6  |-  ( v  =  V  ->  (
( U  e.  ( X I Z )  /\  v  e.  ( Y I Z ) )  <->  ( U  e.  ( X I Z )  /\  V  e.  ( Y I Z ) ) ) )
59 oveq1 6098 . . . . . . . . 9  |-  ( v  =  V  ->  (
v I X )  =  ( V I X ) )
6059eleq2d 2510 . . . . . . . 8  |-  ( v  =  V  ->  (
a  e.  ( v I X )  <->  a  e.  ( V I X ) ) )
6160anbi2d 703 . . . . . . 7  |-  ( v  =  V  ->  (
( a  e.  ( U I Y )  /\  a  e.  ( v I X ) )  <->  ( a  e.  ( U I Y )  /\  a  e.  ( V I X ) ) ) )
6261rexbidv 2736 . . . . . 6  |-  ( v  =  V  ->  ( E. a  e.  P  ( a  e.  ( U I Y )  /\  a  e.  ( v I X ) )  <->  E. a  e.  P  ( a  e.  ( U I Y )  /\  a  e.  ( V I X ) ) ) )
6358, 62imbi12d 320 . . . . 5  |-  ( v  =  V  ->  (
( ( U  e.  ( X I Z )  /\  v  e.  ( Y I Z ) )  ->  E. a  e.  P  ( a  e.  ( U I Y )  /\  a  e.  ( v I X ) ) )  <->  ( ( U  e.  ( X I Z )  /\  V  e.  ( Y I Z ) )  ->  E. a  e.  P  ( a  e.  ( U I Y )  /\  a  e.  ( V I X ) ) ) ) )
6456, 63rspc2v 3079 . . . 4  |-  ( ( U  e.  P  /\  V  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 ) ) )  -> 
( ( U  e.  ( X I Z )  /\  V  e.  ( Y I Z ) )  ->  E. a  e.  P  ( a  e.  ( U I Y )  /\  a  e.  ( V I X ) ) ) ) )
6548, 49, 64syl2anc 661 . . 3  |-  ( ph  ->  ( 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 ) ) )  -> 
( ( U  e.  ( X I Z )  /\  V  e.  ( Y I Z ) )  ->  E. a  e.  P  ( a  e.  ( U I Y )  /\  a  e.  ( V I X ) ) ) ) )
6647, 65mpd 15 . 2  |-  ( ph  ->  ( ( U  e.  ( X I Z )  /\  V  e.  ( Y I Z ) )  ->  E. a  e.  P  ( a  e.  ( U I Y )  /\  a  e.  ( V I X ) ) ) )
671, 2, 66mp2and 679 1  |-  ( ph  ->  E. a  e.  P  ( a  e.  ( U I Y )  /\  a  e.  ( V I X ) ) )
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 2715   E.wrex 2716   {crab 2719   _Vcvv 2972   [.wsbc 3186    \ cdif 3325    i^i cin 3327   ~Pcpw 3860   {csn 3877   ` cfv 5418  (class class class)co 6091    e. cmpt2 6093   Basecbs 14174   distcds 14247  TarskiGcstrkg 22889  TarskiGCcstrkgc 22890  TarskiGBcstrkgb 22891  TarskiGCBcstrkgcb 22892  Itvcitv 22897  LineGclng 22898
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 4421
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 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-sbc 3187  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-iota 5381  df-fv 5426  df-ov 6094  df-trkgb 22910  df-trkg 22916
This theorem is referenced by:  tgbtwncom  22942  tgbtwnswapid  22945  tgbtwnintr  22946  tgtrisegint  22952  tgbtwnconn1  23007  midexlem  23086  f1otrg  23117
  Copyright terms: Public domain W3C validator