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=BaseG
axtrkg.d -˙=distG
axtrkg.i I=ItvG
axtrkg.g φG𝒢Tarski
axtgcont.1 φSP
axtgcont.2 φTP
Assertion axtgcont1 φaPxSyTxaIybPxSyTbxIy

Proof

Step Hyp Ref Expression
1 axtrkg.p P=BaseG
2 axtrkg.d -˙=distG
3 axtrkg.i I=ItvG
4 axtrkg.g φG𝒢Tarski
5 axtgcont.1 φSP
6 axtgcont.2 φTP
7 df-trkg 𝒢Tarski=𝒢TarskiC𝒢TarskiB𝒢TarskiCBf|[˙Basef/p]˙[˙Itvf/i]˙Line𝒢f=xp,ypxzp|zxiyxziyyxiz
8 inss1 𝒢TarskiC𝒢TarskiB𝒢TarskiCBf|[˙Basef/p]˙[˙Itvf/i]˙Line𝒢f=xp,ypxzp|zxiyxziyyxiz𝒢TarskiC𝒢TarskiB
9 inss2 𝒢TarskiC𝒢TarskiB𝒢TarskiB
10 8 9 sstri 𝒢TarskiC𝒢TarskiB𝒢TarskiCBf|[˙Basef/p]˙[˙Itvf/i]˙Line𝒢f=xp,ypxzp|zxiyxziyyxiz𝒢TarskiB
11 7 10 eqsstri 𝒢Tarski𝒢TarskiB
12 11 4 sselid φG𝒢TarskiB
13 1 2 3 istrkgb G𝒢TarskiBGVxPyPyxIxx=yxPyPzPuPvPuxIzvyIzaPauIyavIxs𝒫Pt𝒫PaPxsytxaIybPxsytbxIy
14 13 simprbi G𝒢TarskiBxPyPyxIxx=yxPyPzPuPvPuxIzvyIzaPauIyavIxs𝒫Pt𝒫PaPxsytxaIybPxsytbxIy
15 14 simp3d G𝒢TarskiBs𝒫Pt𝒫PaPxsytxaIybPxsytbxIy
16 12 15 syl φs𝒫Pt𝒫PaPxsytxaIybPxsytbxIy
17 1 fvexi PV
18 17 ssex SPSV
19 elpwg SVS𝒫PSP
20 5 18 19 3syl φS𝒫PSP
21 5 20 mpbird φS𝒫P
22 17 ssex TPTV
23 elpwg TVT𝒫PTP
24 6 22 23 3syl φT𝒫PTP
25 6 24 mpbird φT𝒫P
26 raleq s=SxsytxaIyxSytxaIy
27 26 rexbidv s=SaPxsytxaIyaPxSytxaIy
28 raleq s=SxsytbxIyxSytbxIy
29 28 rexbidv s=SbPxsytbxIybPxSytbxIy
30 27 29 imbi12d s=SaPxsytxaIybPxsytbxIyaPxSytxaIybPxSytbxIy
31 raleq t=TytxaIyyTxaIy
32 31 rexralbidv t=TaPxSytxaIyaPxSyTxaIy
33 raleq t=TytbxIyyTbxIy
34 33 rexralbidv t=TbPxSytbxIybPxSyTbxIy
35 32 34 imbi12d t=TaPxSytxaIybPxSytbxIyaPxSyTxaIybPxSyTbxIy
36 30 35 rspc2v S𝒫PT𝒫Ps𝒫Pt𝒫PaPxsytxaIybPxsytbxIyaPxSyTxaIybPxSyTbxIy
37 21 25 36 syl2anc φs𝒫Pt𝒫PaPxsytxaIybPxsytbxIyaPxSyTxaIybPxSyTbxIy
38 16 37 mpd φaPxSyTxaIybPxSyTbxIy