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 φ G 𝒢 Tarski
axtgcont.1 φ S P
axtgcont.2 φ T P
Assertion axtgcont1 φ a P x S y T x a I y b P x S y T b 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 φ G 𝒢 Tarski
5 axtgcont.1 φ S P
6 axtgcont.2 φ T P
7 df-trkg 𝒢 Tarski = 𝒢 Tarski C 𝒢 Tarski B 𝒢 Tarski CB f | [˙Base f / p]˙ [˙ Itv f / i]˙ Line 𝒢 f = x p , y p x z p | z x i y x z i y y x i z
8 inss1 𝒢 Tarski C 𝒢 Tarski B 𝒢 Tarski CB f | [˙Base f / p]˙ [˙ Itv f / i]˙ Line 𝒢 f = x p , y p x z p | z x i y x z i y y x i z 𝒢 Tarski C 𝒢 Tarski B
9 inss2 𝒢 Tarski C 𝒢 Tarski B 𝒢 Tarski B
10 8 9 sstri 𝒢 Tarski C 𝒢 Tarski B 𝒢 Tarski CB f | [˙Base f / p]˙ [˙ Itv f / i]˙ Line 𝒢 f = x p , y p x z p | z x i y x z i y y x i z 𝒢 Tarski B
11 7 10 eqsstri 𝒢 Tarski 𝒢 Tarski B
12 11 4 sselid φ G 𝒢 Tarski B
13 1 2 3 istrkgb G 𝒢 Tarski B G V x P y P y x I x x = y x P y P z P u P v P u x I z v y I z a P a u I y a v I x s 𝒫 P t 𝒫 P a P x s y t x a I y b P x s y t b x I y
14 13 simprbi G 𝒢 Tarski B x P y P y x I x x = y x P y P z P u P v P u x I z v y I z a P a u I y a v I x s 𝒫 P t 𝒫 P a P x s y t x a I y b P x s y t b x I y
15 14 simp3d G 𝒢 Tarski B s 𝒫 P t 𝒫 P a P x s y t x a I y b P x s y t b x I y
16 12 15 syl φ s 𝒫 P t 𝒫 P a P x s y t x a I y b P x s y t b x I y
17 1 fvexi P V
18 17 ssex S P S V
19 elpwg S V S 𝒫 P S P
20 5 18 19 3syl φ S 𝒫 P S P
21 5 20 mpbird φ S 𝒫 P
22 17 ssex T P T V
23 elpwg T V T 𝒫 P T P
24 6 22 23 3syl φ T 𝒫 P T P
25 6 24 mpbird φ T 𝒫 P
26 raleq s = S x s y t x a I y x S y t x a I y
27 26 rexbidv s = S a P x s y t x a I y a P x S y t x a I y
28 raleq s = S x s y t b x I y x S y t b x I y
29 28 rexbidv s = S b P x s y t b x I y b P x S y t b x I y
30 27 29 imbi12d s = S a P x s y t x a I y b P x s y t b x I y a P x S y t x a I y b P x S y t b x I y
31 raleq t = T y t x a I y y T x a I y
32 31 rexralbidv t = T a P x S y t x a I y a P x S y T x a I y
33 raleq t = T y t b x I y y T b x I y
34 33 rexralbidv t = T b P x S y t b x I y b P x S y T b x I y
35 32 34 imbi12d t = T a P x S y t x a I y b P x S y t b x I y a P x S y T x a I y b P x S y T b x I y
36 30 35 rspc2v S 𝒫 P T 𝒫 P s 𝒫 P t 𝒫 P a P x s y t x a I y b P x s y t b x I y a P x S y T x a I y b P x S y T b x I y
37 21 25 36 syl2anc φ s 𝒫 P t 𝒫 P a P x s y t x a I y b P x s y t b x I y a P x S y T x a I y b P x S y T b x I y
38 16 37 mpd φ a P x S y T x a I y b P x S y T b x I y