MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axtgcont1 Structured version   Visualization version   Unicode version
Theorem axtgcont1 25367
Description: Axiom of Continuity. Axiom A11 of [Schwabhauser] p. 13. This axiom (scheme) asserts that any two sets S and T (of points) such that the elements of S precede the elements of T with respect to some point a (that is, x is between a and y whenever x is in X and y is in Y) are separated by some point b; this is explained in Axiom 11 of [Tarski1999] p. 185. (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 25352 . . . . 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 3833 . . . . . 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 3834 . . . . . 6 |- (TarskiGC i^i TarskiGB ) C_ TarskiGB
42, 3sstri 3612 . . . . 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 3635 . . . 4 |- TarskiG C_ TarskiGB
6 axtrkg.g . . . 4 |- ( ph -> G e. TarskiG )
75, 6sseldi 3601 . . 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 25354 . . . . 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 480 . . . 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 1075 . . 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 17 . 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 6201 . . . . . . 7 |- ( Base ` G ) e. _V
178, 16eqeltri 2697 . . . . . 6 |- P e. _V
1817ssex 4802 . . . . 5 |- ( S C_ P -> S e. _V )
19 elpwg 4166 . . . . 5 |- ( S e. _V -> ( S e. ~P P <-> S C_ P ) )
2015, 18, 193syl 18 . . . 4 |- ( ph -> ( S e. ~P P <-> S C_ P ) )
2115, 20mpbird 247 . . 3 |- ( ph -> S e. ~P P )
22 axtgcont.2 . . . 4 |- ( ph -> T C_ P )
2317ssex 4802 . . . . 5 |- ( T C_ P -> T e. _V )
24 elpwg 4166 . . . . 5 |- ( T e. _V -> ( T e. ~P P <-> T C_ P ) )
2522, 23, 243syl 18 . . . 4 |- ( ph -> ( T e. ~P P <-> T C_ P ) )
2622, 25mpbird 247 . . 3 |- ( ph -> T e. ~P P )
27 raleq 3138 . . . . . 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 3052 . . . . 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 3138 . . . . . 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 3052 . . . . 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 334 . . . 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 3138 . . . . . 6 |- ( t = T -> ( A. y e. t x e. ( a I y ) <-> A. y e. T x e. ( a I y ) ) )
3332rexralbidv 3058 . . . . 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 3138 . . . . . 6 |- ( t = T -> ( A. y e. t b e. ( x I y ) <-> A. y e. T b e. ( x I y ) ) )
3534rexralbidv 3058 . . . . 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 334 . . . 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 3322 . . 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 693 . 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 196   /\ wa 384   \/ w3o 1036   /\ w3a 1037   = wceq 1483   e. wcel 1990   {cab 2608   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   [.wsbc 3435   \ cdif 3571   i^i cin 3573   C_ wss 3574   ~Pcpw 4158   {csn 4177   ` cfv 5888  (class class class)co 6650   |-> cmpt2 6652   Basecbs 15857   distcds 15950  TarskiGcstrkg 25329  TarskiGCcstrkgc 25330  TarskiGBcstrkgb 25331  TarskiGCBcstrkgcb 25332  Itvcitv 25335  LineGclng 25336
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-trkgb 25348  df-trkg 25352
This theorem is referenced by:  axtgcont  25368
  Copyright terms: Public domain W3C validator