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

Theorem axtgcont1 22951
Description: Axiom of Continuity. Axiom A11 of [Schwabhauser] p. 13. (Contributed by Thierry Arnoux, 16-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 )
axtgcont.1  |-  ( ph  ->  S  C_  P )
axtgcont.2  |-  ( ph  ->  T  C_  P )
Assertion
Ref Expression
axtgcont1  |-  ( ph  ->  ( 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 ) ) )
Distinct variable groups:    x, y    a, b, x, y, I    P, a, b, x, y    S, a, b, x    T, a, b, x, y    .- , a,
b, x, y
Allowed substitution hints:    ph( x, y, a, b)    S( y)    G( x, y, a, b)

Proof of Theorem axtgcont1
Dummy variables  f 
i  p  z  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 ) ) ) )
1312simp3d 1002 . . 3  |-  ( G  e. TarskiGB 
->  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 ) ) )
147, 13syl 16 . 2  |-  ( ph  ->  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 ) ) )
15 axtgcont.1 . . . 4  |-  ( ph  ->  S  C_  P )
16 fvex 5722 . . . . . . 7  |-  ( Base `  G )  e.  _V
178, 16eqeltri 2513 . . . . . 6  |-  P  e. 
_V
1817ssex 4457 . . . . 5  |-  ( S 
C_  P  ->  S  e.  _V )
19 elpwg 3889 . . . . 5  |-  ( S  e.  _V  ->  ( S  e.  ~P P  <->  S 
C_  P ) )
2015, 18, 193syl 20 . . . 4  |-  ( ph  ->  ( S  e.  ~P P 
<->  S  C_  P )
)
2115, 20mpbird 232 . . 3  |-  ( ph  ->  S  e.  ~P P
)
22 axtgcont.2 . . . 4  |-  ( ph  ->  T  C_  P )
2317ssex 4457 . . . . 5  |-  ( T 
C_  P  ->  T  e.  _V )
24 elpwg 3889 . . . . 5  |-  ( T  e.  _V  ->  ( T  e.  ~P P  <->  T 
C_  P ) )
2522, 23, 243syl 20 . . . 4  |-  ( ph  ->  ( T  e.  ~P P 
<->  T  C_  P )
)
2622, 25mpbird 232 . . 3  |-  ( ph  ->  T  e.  ~P P
)
27 raleq 2938 . . . . . 6  |-  ( s  =  S  ->  ( A. x  e.  s  A. y  e.  t  x  e.  ( a
I y )  <->  A. x  e.  S  A. y  e.  t  x  e.  ( a I y ) ) )
2827rexbidv 2757 . . . . 5  |-  ( s  =  S  ->  ( E. a  e.  P  A. x  e.  s  A. y  e.  t  x  e.  ( a
I y )  <->  E. a  e.  P  A. x  e.  S  A. y  e.  t  x  e.  ( a I y ) ) )
29 raleq 2938 . . . . . 6  |-  ( s  =  S  ->  ( A. x  e.  s  A. y  e.  t 
b  e.  ( x I y )  <->  A. x  e.  S  A. y  e.  t  b  e.  ( x I y ) ) )
3029rexbidv 2757 . . . . 5  |-  ( s  =  S  ->  ( E. b  e.  P  A. x  e.  s  A. y  e.  t 
b  e.  ( x I y )  <->  E. b  e.  P  A. x  e.  S  A. y  e.  t  b  e.  ( x I y ) ) )
3128, 30imbi12d 320 . . . 4  |-  ( s  =  S  ->  (
( 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 ) )  <-> 
( 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 ) ) ) )
32 raleq 2938 . . . . . 6  |-  ( t  =  T  ->  ( A. y  e.  t  x  e.  ( a
I y )  <->  A. y  e.  T  x  e.  ( a I y ) ) )
3332rexralbidv 2780 . . . . 5  |-  ( t  =  T  ->  ( E. a  e.  P  A. x  e.  S  A. y  e.  t  x  e.  ( a
I y )  <->  E. a  e.  P  A. x  e.  S  A. y  e.  T  x  e.  ( a I y ) ) )
34 raleq 2938 . . . . . 6  |-  ( t  =  T  ->  ( A. y  e.  t 
b  e.  ( x I y )  <->  A. y  e.  T  b  e.  ( x I y ) ) )
3534rexralbidv 2780 . . . . 5  |-  ( t  =  T  ->  ( E. b  e.  P  A. x  e.  S  A. y  e.  t 
b  e.  ( x I y )  <->  E. b  e.  P  A. x  e.  S  A. y  e.  T  b  e.  ( x I y ) ) )
3633, 35imbi12d 320 . . . 4  |-  ( t  =  T  ->  (
( 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 ) )  <-> 
( 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 ) ) ) )
3731, 36rspc2v 3100 . . 3  |-  ( ( S  e.  ~P P  /\  T  e.  ~P P )  ->  ( 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 ) )  ->  ( 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 ) ) ) )
3821, 26, 37syl2anc 661 . 2  |-  ( ph  ->  ( 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 ) )  ->  ( 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 ) ) ) )
3914, 38mpd 15 1  |-  ( ph  ->  ( 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 ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ 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    C_ wss 3349   ~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-sep 4434  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:  axtgcont  22952
  Copyright terms: Public domain W3C validator