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

Theorem axtgpasch 23730
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 23716 . . . . . . 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 3723 . . . . . . . 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 3724 . . . . . . . 8  |-  (TarskiGC  i^i TarskiGB )  C_ TarskiGB
64, 5sstri 3518 . . . . . . 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 3539 . . . . . 6  |- TarskiG  C_ TarskiGB
8 axtrkg.g . . . . . 6  |-  ( ph  ->  G  e. TarskiG )
97, 8sseldi 3507 . . . . 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 23718 . . . . . . 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 1009 . . . . 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 6302 . . . . . . . . . 10  |-  ( x  =  X  ->  (
x I z )  =  ( X I z ) )
2120eleq2d 2537 . . . . . . . . 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 6303 . . . . . . . . . . 11  |-  ( x  =  X  ->  (
v I x )  =  ( v I X ) )
2423eleq2d 2537 . . . . . . . . . 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 2978 . . . . . . . 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 2911 . . . . . 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 6302 . . . . . . . . . 10  |-  ( y  =  Y  ->  (
y I z )  =  ( Y I z ) )
3029eleq2d 2537 . . . . . . . . 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 6303 . . . . . . . . . . 11  |-  ( y  =  Y  ->  (
u I y )  =  ( u I Y ) )
3332eleq2d 2537 . . . . . . . . . 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 2978 . . . . . . . 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 2911 . . . . . 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 6303 . . . . . . . . . 10  |-  ( z  =  Z  ->  ( X I z )  =  ( X I Z ) )
3938eleq2d 2537 . . . . . . . . 9  |-  ( z  =  Z  ->  (
u  e.  ( X I z )  <->  u  e.  ( X I Z ) ) )
40 oveq2 6303 . . . . . . . . . 10  |-  ( z  =  Z  ->  ( Y I z )  =  ( Y I Z ) )
4140eleq2d 2537 . . . . . . . . 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 2911 . . . . . 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 3231 . . . . 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 1228 . . . 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 2539 . . . . . . 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 6302 . . . . . . . . 9  |-  ( u  =  U  ->  (
u I Y )  =  ( U I Y ) )
5352eleq2d 2537 . . . . . . . 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 2978 . . . . . 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 2539 . . . . . . 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 6302 . . . . . . . . 9  |-  ( v  =  V  ->  (
v I X )  =  ( V I X ) )
6059eleq2d 2537 . . . . . . . 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 2978 . . . . . 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 3228 . . . 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 972    /\ w3a 973    = wceq 1379    e. wcel 1767   {cab 2452   A.wral 2817   E.wrex 2818   {crab 2821   _Vcvv 3118   [.wsbc 3336    \ cdif 3478    i^i cin 3480   ~Pcpw 4016   {csn 4033   ` cfv 5594  (class class class)co 6295    |-> cmpt2 6297   Basecbs 14507   distcds 14581  TarskiGcstrkg 23691  TarskiGCcstrkgc 23692  TarskiGBcstrkgb 23693  TarskiGCBcstrkgcb 23694  Itvcitv 23698  LineGclng 23699
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-nul 4582
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-sbc 3337  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-op 4040  df-uni 4252  df-br 4454  df-iota 5557  df-fv 5602  df-ov 6298  df-trkgb 23711  df-trkg 23716
This theorem is referenced by:  tgbtwncom  23745  tgbtwnswapid  23749  tgbtwnintr  23750  tgtrisegint  23756  tgbtwnconn1  23827  midexlem  23917  opphllem  23954  opphllem1  23959  f1otrg  23997
  Copyright terms: Public domain W3C validator