df-trkgb

Description: Define the class of geometries fulfilling the 3 betweenness axioms in Tarski's Axiomatization of Geometry: identity, Axiom A6 of Schwabhauser p. 11, axiom of Pasch, Axiom A7 of Schwabhauser p. 12, and continuity, Axiom A11 of Schwabhauser p. 13. (Contributed by Thierry Arnoux, 24-Aug-2017)

		Ref	Expression
	Assertion	df-trkgb	$⊢ 𝒢_{Tarski}^{B} = \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} (\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)))\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cstrkgb	$class 𝒢_{Tarski}^{B}$
1		vf	$setvar f$
2		cbs	$class Base$
3	1	cv	$setvar f$
4	3 2	cfv	$class {Base}_{f}$
5		vp	$setvar p$
6		citv	$class Itv$
7	3 6	cfv	$class Itv (f)$
8		vi	$setvar i$
9		vx	$setvar x$
10	5	cv	$setvar p$
11		vy	$setvar y$
12	11	cv	$setvar y$
13	9	cv	$setvar x$
14	8	cv	$setvar i$
15	13 13 14	co	$class (x i x)$
16	12 15	wcel	$wff y \in (x i x)$
17	13 12	wceq	$wff x = y$
18	16 17	wi	$wff (y \in (x i x) \to x = y)$
19	18 11 10	wral	$wff \forall y \in p (y \in (x i x) \to x = y)$
20	19 9 10	wral	$wff \forall x \in p \forall y \in p (y \in (x i x) \to x = y)$
21		vz	$setvar z$
22		vu	$setvar u$
23		vv	$setvar v$
24	22	cv	$setvar u$
25	21	cv	$setvar z$
26	13 25 14	co	$class (x i z)$
27	24 26	wcel	$wff u \in (x i z)$
28	23	cv	$setvar v$
29	12 25 14	co	$class (y i z)$
30	28 29	wcel	$wff v \in (y i z)$
31	27 30	wa	$wff (u \in (x i z) \land v \in (y i z))$
32		va	$setvar a$
33	32	cv	$setvar a$
34	24 12 14	co	$class (u i y)$
35	33 34	wcel	$wff a \in (u i y)$
36	28 13 14	co	$class (v i x)$
37	33 36	wcel	$wff a \in (v i x)$
38	35 37	wa	$wff (a \in (u i y) \land a \in (v i x))$
39	38 32 10	wrex	$wff \exists a \in p (a \in (u i y) \land a \in (v i x))$
40	31 39	wi	$wff ((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)))$
41	40 23 10	wral	$wff \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)))$
42	41 22 10	wral	$wff \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)))$
43	42 21 10	wral	$wff \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)))$
44	43 11 10	wral	$wff \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)))$
45	44 9 10	wral	$wff \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)))$
46		vs	$setvar s$
47	10	cpw	$class 𝒫 p$
48		vt	$setvar t$
49	46	cv	$setvar s$
50	48	cv	$setvar t$
51	33 12 14	co	$class (a i y)$
52	13 51	wcel	$wff x \in (a i y)$
53	52 11 50	wral	$wff \forall y \in t x \in (a i y)$
54	53 9 49	wral	$wff \forall x \in s \forall y \in t x \in (a i y)$
55	54 32 10	wrex	$wff \exists a \in p \forall x \in s \forall y \in t x \in (a i y)$
56		vb	$setvar b$
57	56	cv	$setvar b$
58	13 12 14	co	$class (x i y)$
59	57 58	wcel	$wff b \in (x i y)$
60	59 11 50	wral	$wff \forall y \in t b \in (x i y)$
61	60 9 49	wral	$wff \forall x \in s \forall y \in t b \in (x i y)$
62	61 56 10	wrex	$wff \exists b \in p \forall x \in s \forall y \in t b \in (x i y)$
63	55 62	wi	$wff (\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))$
64	63 48 47	wral	$wff \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))$
65	64 46 47	wral	$wff \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))$
66	20 45 65	w3a	$wff (\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)))$
67	66 8 7	wsbc	$wff \underset{˙}{[} Itv (f) / i \underset{˙}{]} (\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)))$
68	67 5 4	wsbc	$wff \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} (\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)))$
69	68 1	cab	$class \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} (\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)))\}$
70	0 69	wceq	$wff 𝒢_{Tarski}^{B} = \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} (\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)))\}$

Metamath Proof Explorer

Definition df-trkgb

Detailed syntax breakdown