Metamath Proof Explorer


Theorem axtgcont1

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)

Ref Expression
Hypotheses 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 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 ) ) )

Proof

Step Hyp Ref Expression
1 axtrkg.p
 |-  P = ( Base ` G )
2 axtrkg.d
 |-  .- = ( dist ` G )
3 axtrkg.i
 |-  I = ( Itv ` G )
4 axtrkg.g
 |-  ( ph -> G e. TarskiG )
5 axtgcont.1
 |-  ( ph -> S C_ P )
6 axtgcont.2
 |-  ( ph -> T C_ P )
7 df-trkg
 |-  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 ) ) } ) } ) )
8 inss1
 |-  ( ( 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 )
9 inss2
 |-  ( TarskiGC i^i TarskiGB ) C_ TarskiGB
10 8 9 sstri
 |-  ( ( 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
11 7 10 eqsstri
 |-  TarskiG C_ TarskiGB
12 11 4 sselid
 |-  ( ph -> G e. TarskiGB )
13 1 2 3 istrkgb
 |-  ( 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 ) ) ) ) )
14 13 simprbi
 |-  ( 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 ) ) ) )
15 14 simp3d
 |-  ( 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 ) ) )
16 12 15 syl
 |-  ( 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 ) ) )
17 1 fvexi
 |-  P e. _V
18 17 ssex
 |-  ( S C_ P -> S e. _V )
19 elpwg
 |-  ( S e. _V -> ( S e. ~P P <-> S C_ P ) )
20 5 18 19 3syl
 |-  ( ph -> ( S e. ~P P <-> S C_ P ) )
21 5 20 mpbird
 |-  ( ph -> S e. ~P P )
22 17 ssex
 |-  ( T C_ P -> T e. _V )
23 elpwg
 |-  ( T e. _V -> ( T e. ~P P <-> T C_ P ) )
24 6 22 23 3syl
 |-  ( ph -> ( T e. ~P P <-> T C_ P ) )
25 6 24 mpbird
 |-  ( ph -> T e. ~P P )
26 raleq
 |-  ( 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 ) ) )
27 26 rexbidv
 |-  ( 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 ) ) )
28 raleq
 |-  ( 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 ) ) )
29 28 rexbidv
 |-  ( 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 ) ) )
30 27 29 imbi12d
 |-  ( 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 ) ) ) )
31 raleq
 |-  ( t = T -> ( A. y e. t x e. ( a I y ) <-> A. y e. T x e. ( a I y ) ) )
32 31 rexralbidv
 |-  ( 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 ) ) )
33 raleq
 |-  ( t = T -> ( A. y e. t b e. ( x I y ) <-> A. y e. T b e. ( x I y ) ) )
34 33 rexralbidv
 |-  ( 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 ) ) )
35 32 34 imbi12d
 |-  ( 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 ) ) ) )
36 30 35 rspc2v
 |-  ( ( 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 ) ) ) )
37 21 25 36 syl2anc
 |-  ( 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 ) ) ) )
38 16 37 mpd
 |-  ( 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 ) ) )