Definition df-trkgb 28457

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.)

Assertion

Ref	Expression
df-trkgb	⊢ TarskiGB = {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎 ∈ 𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝑝∀𝑡 ∈ 𝒫 𝑝(∃𝑎 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝑖𝑦) → ∃𝑏 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝑖𝑦)))}

Distinct variable group:   𝑎,𝑏,𝑓,𝑝,𝑖,𝑠,𝑡,𝑢,𝑣,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-trkgb

Step	Hyp	Ref	Expression
1		cstrkgb 28437	. 2 class TarskiGB
2		vy	. . . . . . . . . . 11 setvar 𝑦
3	2	cv 1539	. . . . . . . . . 10 class 𝑦
4		vx	. . . . . . . . . . . 12 setvar 𝑥
5	4	cv 1539	. . . . . . . . . . 11 class 𝑥
6		vi	. . . . . . . . . . . 12 setvar 𝑖
7	6	cv 1539	. . . . . . . . . . 11 class 𝑖
8	5, 5, 7	co 7431	. . . . . . . . . 10 class (𝑥𝑖𝑥)
9	3, 8	wcel 2108	. . . . . . . . 9 wff 𝑦 ∈ (𝑥𝑖𝑥)
10	4, 2	weq 1962	. . . . . . . . 9 wff 𝑥 = 𝑦
11	9, 10	wi 4	. . . . . . . 8 wff (𝑦 ∈ (𝑥𝑖𝑥) → 𝑥 = 𝑦)
12		vp	. . . . . . . . 9 setvar 𝑝
13	12	cv 1539	. . . . . . . 8 class 𝑝
14	11, 2, 13	wral 3061	. . . . . . 7 wff ∀𝑦 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑥) → 𝑥 = 𝑦)
15	14, 4, 13	wral 3061	. . . . . 6 wff ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑥) → 𝑥 = 𝑦)
16		vu	. . . . . . . . . . . . . . 15 setvar 𝑢
17	16	cv 1539	. . . . . . . . . . . . . 14 class 𝑢
18		vz	. . . . . . . . . . . . . . . 16 setvar 𝑧
19	18	cv 1539	. . . . . . . . . . . . . . 15 class 𝑧
20	5, 19, 7	co 7431	. . . . . . . . . . . . . 14 class (𝑥𝑖𝑧)
21	17, 20	wcel 2108	. . . . . . . . . . . . 13 wff 𝑢 ∈ (𝑥𝑖𝑧)
22		vv	. . . . . . . . . . . . . . 15 setvar 𝑣
23	22	cv 1539	. . . . . . . . . . . . . 14 class 𝑣
24	3, 19, 7	co 7431	. . . . . . . . . . . . . 14 class (𝑦𝑖𝑧)
25	23, 24	wcel 2108	. . . . . . . . . . . . 13 wff 𝑣 ∈ (𝑦𝑖𝑧)
26	21, 25	wa 395	. . . . . . . . . . . 12 wff (𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧))
27		va	. . . . . . . . . . . . . . . 16 setvar 𝑎
28	27	cv 1539	. . . . . . . . . . . . . . 15 class 𝑎
29	17, 3, 7	co 7431	. . . . . . . . . . . . . . 15 class (𝑢𝑖𝑦)
30	28, 29	wcel 2108	. . . . . . . . . . . . . 14 wff 𝑎 ∈ (𝑢𝑖𝑦)
31	23, 5, 7	co 7431	. . . . . . . . . . . . . . 15 class (𝑣𝑖𝑥)
32	28, 31	wcel 2108	. . . . . . . . . . . . . 14 wff 𝑎 ∈ (𝑣𝑖𝑥)
33	30, 32	wa 395	. . . . . . . . . . . . 13 wff (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥))
34	33, 27, 13	wrex 3070	. . . . . . . . . . . 12 wff ∃𝑎 ∈ 𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥))
35	26, 34	wi 4	. . . . . . . . . . 11 wff ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎 ∈ 𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥)))
36	35, 22, 13	wral 3061	. . . . . . . . . 10 wff ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎 ∈ 𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥)))
37	36, 16, 13	wral 3061	. . . . . . . . 9 wff ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎 ∈ 𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥)))
38	37, 18, 13	wral 3061	. . . . . . . 8 wff ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎 ∈ 𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥)))
39	38, 2, 13	wral 3061	. . . . . . 7 wff ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎 ∈ 𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥)))
40	39, 4, 13	wral 3061	. . . . . 6 wff ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎 ∈ 𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥)))
41	28, 3, 7	co 7431	. . . . . . . . . . . . 13 class (𝑎𝑖𝑦)
42	5, 41	wcel 2108	. . . . . . . . . . . 12 wff 𝑥 ∈ (𝑎𝑖𝑦)
43		vt	. . . . . . . . . . . . 13 setvar 𝑡
44	43	cv 1539	. . . . . . . . . . . 12 class 𝑡
45	42, 2, 44	wral 3061	. . . . . . . . . . 11 wff ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝑖𝑦)
46		vs	. . . . . . . . . . . 12 setvar 𝑠
47	46	cv 1539	. . . . . . . . . . 11 class 𝑠
48	45, 4, 47	wral 3061	. . . . . . . . . 10 wff ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝑖𝑦)
49	48, 27, 13	wrex 3070	. . . . . . . . 9 wff ∃𝑎 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝑖𝑦)
50		vb	. . . . . . . . . . . . . 14 setvar 𝑏
51	50	cv 1539	. . . . . . . . . . . . 13 class 𝑏
52	5, 3, 7	co 7431	. . . . . . . . . . . . 13 class (𝑥𝑖𝑦)
53	51, 52	wcel 2108	. . . . . . . . . . . 12 wff 𝑏 ∈ (𝑥𝑖𝑦)
54	53, 2, 44	wral 3061	. . . . . . . . . . 11 wff ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝑖𝑦)
55	54, 4, 47	wral 3061	. . . . . . . . . 10 wff ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝑖𝑦)
56	55, 50, 13	wrex 3070	. . . . . . . . 9 wff ∃𝑏 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝑖𝑦)
57	49, 56	wi 4	. . . . . . . 8 wff (∃𝑎 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝑖𝑦) → ∃𝑏 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝑖𝑦))
58	13	cpw 4600	. . . . . . . 8 class 𝒫 𝑝
59	57, 43, 58	wral 3061	. . . . . . 7 wff ∀𝑡 ∈ 𝒫 𝑝(∃𝑎 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝑖𝑦) → ∃𝑏 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝑖𝑦))
60	59, 46, 58	wral 3061	. . . . . 6 wff ∀𝑠 ∈ 𝒫 𝑝∀𝑡 ∈ 𝒫 𝑝(∃𝑎 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝑖𝑦) → ∃𝑏 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝑖𝑦))
61	15, 40, 60	w3a 1087	. . . . 5 wff (∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎 ∈ 𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝑝∀𝑡 ∈ 𝒫 𝑝(∃𝑎 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝑖𝑦) → ∃𝑏 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝑖𝑦)))
62		vf	. . . . . . 7 setvar 𝑓
63	62	cv 1539	. . . . . 6 class 𝑓
64		citv 28441	. . . . . 6 class Itv
65	63, 64	cfv 6561	. . . . 5 class (Itv‘𝑓)
66	61, 6, 65	wsbc 3788	. . . 4 wff [(Itv‘𝑓) / 𝑖](∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎 ∈ 𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝑝∀𝑡 ∈ 𝒫 𝑝(∃𝑎 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝑖𝑦) → ∃𝑏 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝑖𝑦)))
67		cbs 17247	. . . . 5 class Base
68	63, 67	cfv 6561	. . . 4 class (Base‘𝑓)
69	66, 12, 68	wsbc 3788	. . 3 wff [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎 ∈ 𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝑝∀𝑡 ∈ 𝒫 𝑝(∃𝑎 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝑖𝑦) → ∃𝑏 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝑖𝑦)))
70	69, 62	cab 2714	. 2 class {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎 ∈ 𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝑝∀𝑡 ∈ 𝒫 𝑝(∃𝑎 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝑖𝑦) → ∃𝑏 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝑖𝑦)))}
71	1, 70	wceq 1540	1 wff TarskiGB = {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎 ∈ 𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝑝∀𝑡 ∈ 𝒫 𝑝(∃𝑎 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝑖𝑦) → ∃𝑏 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝑖𝑦)))}

This definition is referenced by:  istrkgb  28463