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	$⊢ \underset{˙}{-} = dist (G)$
	axtrkg.i	$⊢ I = Itv (G)$
	axtrkg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	axtgcont.1	$⊢ φ \to S \subseteq P$
	axtgcont.2	$⊢ φ \to T \subseteq P$
Assertion	axtgcont1	$⊢ φ \to (\exists a \in P \forall x \in S \forall y \in T x \in (a I y) \to \exists b \in P \forall x \in S \forall y \in T b \in (x I y))$

Proof

Step	Hyp	Ref	Expression
1		axtrkg.p	$⊢ P = {Base}_{G}$
2		axtrkg.d	$⊢ \underset{˙}{-} = dist (G)$
3		axtrkg.i	$⊢ I = Itv (G)$
4		axtrkg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		axtgcont.1	$⊢ φ \to S \subseteq P$
6		axtgcont.2	$⊢ φ \to T \subseteq P$
7		df-trkg	$⊢ 𝒢_{Tarski} = (𝒢_{Tarski}^{C} \cap 𝒢_{Tarski}^{B}) \cap (𝒢_{Tarski}^{CB} \cap \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\})$
8		inss1	$⊢ (𝒢_{Tarski}^{C} \cap 𝒢_{Tarski}^{B}) \cap (𝒢_{Tarski}^{CB} \cap \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\}) \subseteq 𝒢_{Tarski}^{C} \cap 𝒢_{Tarski}^{B}$
9		inss2	$⊢ 𝒢_{Tarski}^{C} \cap 𝒢_{Tarski}^{B} \subseteq 𝒢_{Tarski}^{B}$
10	8 9	sstri	$⊢ (𝒢_{Tarski}^{C} \cap 𝒢_{Tarski}^{B}) \cap (𝒢_{Tarski}^{CB} \cap \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\}) \subseteq 𝒢_{Tarski}^{B}$
11	7 10	eqsstri	$⊢ 𝒢_{Tarski} \subseteq 𝒢_{Tarski}^{B}$
12	11 4	sselid	$⊢ φ \to G \in 𝒢_{Tarski}^{B}$
13	1 2 3	istrkgb	$⊢ G \in 𝒢_{Tarski}^{B} \leftrightarrow (G \in V \land (\forall x \in P \forall y \in P (y \in (x I x) \to x = y) \land \forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall v \in P ((u \in (x I z) \land v \in (y I z)) \to \exists a \in P (a \in (u I y) \land a \in (v I x))) \land \forall s \in 𝒫 P \forall t \in 𝒫 P (\exists a \in P \forall x \in s \forall y \in t x \in (a I y) \to \exists b \in P \forall x \in s \forall y \in t b \in (x I y))))$
14	13	simprbi	$⊢ G \in 𝒢_{Tarski}^{B} \to (\forall x \in P \forall y \in P (y \in (x I x) \to x = y) \land \forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall v \in P ((u \in (x I z) \land v \in (y I z)) \to \exists a \in P (a \in (u I y) \land a \in (v I x))) \land \forall s \in 𝒫 P \forall t \in 𝒫 P (\exists a \in P \forall x \in s \forall y \in t x \in (a I y) \to \exists b \in P \forall x \in s \forall y \in t b \in (x I y)))$
15	14	simp3d	$⊢ G \in 𝒢_{Tarski}^{B} \to \forall s \in 𝒫 P \forall t \in 𝒫 P (\exists a \in P \forall x \in s \forall y \in t x \in (a I y) \to \exists b \in P \forall x \in s \forall y \in t b \in (x I y))$
16	12 15	syl	$⊢ φ \to \forall s \in 𝒫 P \forall t \in 𝒫 P (\exists a \in P \forall x \in s \forall y \in t x \in (a I y) \to \exists b \in P \forall x \in s \forall y \in t b \in (x I y))$
17	1	fvexi	$⊢ P \in V$
18	17	ssex	$⊢ S \subseteq P \to S \in V$
19		elpwg	$⊢ S \in V \to (S \in 𝒫 P \leftrightarrow S \subseteq P)$
20	5 18 19	3syl	$⊢ φ \to (S \in 𝒫 P \leftrightarrow S \subseteq P)$
21	5 20	mpbird	$⊢ φ \to S \in 𝒫 P$
22	17	ssex	$⊢ T \subseteq P \to T \in V$
23		elpwg	$⊢ T \in V \to (T \in 𝒫 P \leftrightarrow T \subseteq P)$
24	6 22 23	3syl	$⊢ φ \to (T \in 𝒫 P \leftrightarrow T \subseteq P)$
25	6 24	mpbird	$⊢ φ \to T \in 𝒫 P$
26		raleq	$⊢ s = S \to (\forall x \in s \forall y \in t x \in (a I y) \leftrightarrow \forall x \in S \forall y \in t x \in (a I y))$
27	26	rexbidv	$⊢ s = S \to (\exists a \in P \forall x \in s \forall y \in t x \in (a I y) \leftrightarrow \exists a \in P \forall x \in S \forall y \in t x \in (a I y))$
28		raleq	$⊢ s = S \to (\forall x \in s \forall y \in t b \in (x I y) \leftrightarrow \forall x \in S \forall y \in t b \in (x I y))$
29	28	rexbidv	$⊢ s = S \to (\exists b \in P \forall x \in s \forall y \in t b \in (x I y) \leftrightarrow \exists b \in P \forall x \in S \forall y \in t b \in (x I y))$
30	27 29	imbi12d	$⊢ s = S \to ((\exists a \in P \forall x \in s \forall y \in t x \in (a I y) \to \exists b \in P \forall x \in s \forall y \in t b \in (x I y)) \leftrightarrow (\exists a \in P \forall x \in S \forall y \in t x \in (a I y) \to \exists b \in P \forall x \in S \forall y \in t b \in (x I y)))$
31		raleq	$⊢ t = T \to (\forall y \in t x \in (a I y) \leftrightarrow \forall y \in T x \in (a I y))$
32	31	rexralbidv	$⊢ t = T \to (\exists a \in P \forall x \in S \forall y \in t x \in (a I y) \leftrightarrow \exists a \in P \forall x \in S \forall y \in T x \in (a I y))$
33		raleq	$⊢ t = T \to (\forall y \in t b \in (x I y) \leftrightarrow \forall y \in T b \in (x I y))$
34	33	rexralbidv	$⊢ t = T \to (\exists b \in P \forall x \in S \forall y \in t b \in (x I y) \leftrightarrow \exists b \in P \forall x \in S \forall y \in T b \in (x I y))$
35	32 34	imbi12d	$⊢ t = T \to ((\exists a \in P \forall x \in S \forall y \in t x \in (a I y) \to \exists b \in P \forall x \in S \forall y \in t b \in (x I y)) \leftrightarrow (\exists a \in P \forall x \in S \forall y \in T x \in (a I y) \to \exists b \in P \forall x \in S \forall y \in T b \in (x I y)))$
36	30 35	rspc2v	$⊢ (S \in 𝒫 P \land T \in 𝒫 P) \to (\forall s \in 𝒫 P \forall t \in 𝒫 P (\exists a \in P \forall x \in s \forall y \in t x \in (a I y) \to \exists b \in P \forall x \in s \forall y \in t b \in (x I y)) \to (\exists a \in P \forall x \in S \forall y \in T x \in (a I y) \to \exists b \in P \forall x \in S \forall y \in T b \in (x I y)))$
37	21 25 36	syl2anc	$⊢ φ \to (\forall s \in 𝒫 P \forall t \in 𝒫 P (\exists a \in P \forall x \in s \forall y \in t x \in (a I y) \to \exists b \in P \forall x \in s \forall y \in t b \in (x I y)) \to (\exists a \in P \forall x \in S \forall y \in T x \in (a I y) \to \exists b \in P \forall x \in S \forall y \in T b \in (x I y)))$
38	16 37	mpd	$⊢ φ \to (\exists a \in P \forall x \in S \forall y \in T x \in (a I y) \to \exists b \in P \forall x \in S \forall y \in T b \in (x I y))$

Metamath Proof Explorer

Theorem axtgcont1

Proof