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 | |
|
axtrkg.d | |
||
axtrkg.i | |
||
axtrkg.g | |
||
axtgcont.1 | |
||
axtgcont.2 | |
||
Assertion | axtgcont1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | axtrkg.p | |
|
2 | axtrkg.d | |
|
3 | axtrkg.i | |
|
4 | axtrkg.g | |
|
5 | axtgcont.1 | |
|
6 | axtgcont.2 | |
|
7 | df-trkg | |
|
8 | inss1 | |
|
9 | inss2 | |
|
10 | 8 9 | sstri | |
11 | 7 10 | eqsstri | |
12 | 11 4 | sselid | |
13 | 1 2 3 | istrkgb | |
14 | 13 | simprbi | |
15 | 14 | simp3d | |
16 | 12 15 | syl | |
17 | 1 | fvexi | |
18 | 17 | ssex | |
19 | elpwg | |
|
20 | 5 18 19 | 3syl | |
21 | 5 20 | mpbird | |
22 | 17 | ssex | |
23 | elpwg | |
|
24 | 6 22 23 | 3syl | |
25 | 6 24 | mpbird | |
26 | raleq | |
|
27 | 26 | rexbidv | |
28 | raleq | |
|
29 | 28 | rexbidv | |
30 | 27 29 | imbi12d | |
31 | raleq | |
|
32 | 31 | rexralbidv | |
33 | raleq | |
|
34 | 33 | rexralbidv | |
35 | 32 34 | imbi12d | |
36 | 30 35 | rspc2v | |
37 | 21 25 36 | syl2anc | |
38 | 16 37 | mpd | |