Definition df-trkge 27682

Description: Define the class of geometries fulfilling Euclid's axiom, Axiom A10 of [Schwabhauser] p. 13. (Contributed by Thierry Arnoux, 14-Mar-2019.)

Assertion

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

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

Detailed syntax breakdown of Definition df-trkge

Step	Hyp	Ref	Expression
1		cstrkge 27663	. 2 class TarskiGE
2		vu	. . . . . . . . . . . . . 14 setvar 𝑢
3	2	cv 1541	. . . . . . . . . . . . 13 class 𝑢
4		vx	. . . . . . . . . . . . . . 15 setvar 𝑥
5	4	cv 1541	. . . . . . . . . . . . . 14 class 𝑥
6		vv	. . . . . . . . . . . . . . 15 setvar 𝑣
7	6	cv 1541	. . . . . . . . . . . . . 14 class 𝑣
8		vi	. . . . . . . . . . . . . . 15 setvar 𝑖
9	8	cv 1541	. . . . . . . . . . . . . 14 class 𝑖
10	5, 7, 9	co 7404	. . . . . . . . . . . . 13 class (𝑥𝑖𝑣)
11	3, 10	wcel 2107	. . . . . . . . . . . 12 wff 𝑢 ∈ (𝑥𝑖𝑣)
12		vy	. . . . . . . . . . . . . . 15 setvar 𝑦
13	12	cv 1541	. . . . . . . . . . . . . 14 class 𝑦
14		vz	. . . . . . . . . . . . . . 15 setvar 𝑧
15	14	cv 1541	. . . . . . . . . . . . . 14 class 𝑧
16	13, 15, 9	co 7404	. . . . . . . . . . . . 13 class (𝑦𝑖𝑧)
17	3, 16	wcel 2107	. . . . . . . . . . . 12 wff 𝑢 ∈ (𝑦𝑖𝑧)
18	5, 3	wne 2941	. . . . . . . . . . . 12 wff 𝑥 ≠ 𝑢
19	11, 17, 18	w3a 1088	. . . . . . . . . . 11 wff (𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢)
20		va	. . . . . . . . . . . . . . . . 17 setvar 𝑎
21	20	cv 1541	. . . . . . . . . . . . . . . 16 class 𝑎
22	5, 21, 9	co 7404	. . . . . . . . . . . . . . 15 class (𝑥𝑖𝑎)
23	13, 22	wcel 2107	. . . . . . . . . . . . . 14 wff 𝑦 ∈ (𝑥𝑖𝑎)
24		vb	. . . . . . . . . . . . . . . . 17 setvar 𝑏
25	24	cv 1541	. . . . . . . . . . . . . . . 16 class 𝑏
26	5, 25, 9	co 7404	. . . . . . . . . . . . . . 15 class (𝑥𝑖𝑏)
27	15, 26	wcel 2107	. . . . . . . . . . . . . 14 wff 𝑧 ∈ (𝑥𝑖𝑏)
28	21, 25, 9	co 7404	. . . . . . . . . . . . . . 15 class (𝑎𝑖𝑏)
29	7, 28	wcel 2107	. . . . . . . . . . . . . 14 wff 𝑣 ∈ (𝑎𝑖𝑏)
30	23, 27, 29	w3a 1088	. . . . . . . . . . . . 13 wff (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏))
31		vp	. . . . . . . . . . . . . 14 setvar 𝑝
32	31	cv 1541	. . . . . . . . . . . . 13 class 𝑝
33	30, 24, 32	wrex 3071	. . . . . . . . . . . 12 wff ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏))
34	33, 20, 32	wrex 3071	. . . . . . . . . . 11 wff ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏))
35	19, 34	wi 4	. . . . . . . . . 10 wff ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)))
36	35, 6, 32	wral 3062	. . . . . . . . 9 wff ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)))
37	36, 2, 32	wral 3062	. . . . . . . 8 wff ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)))
38	37, 14, 32	wral 3062	. . . . . . 7 wff ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)))
39	38, 12, 32	wral 3062	. . . . . 6 wff ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)))
40	39, 4, 32	wral 3062	. . . . 5 wff ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)))
41		vf	. . . . . . 7 setvar 𝑓
42	41	cv 1541	. . . . . 6 class 𝑓
43		citv 27664	. . . . . 6 class Itv
44	42, 43	cfv 6540	. . . . 5 class (Itv‘𝑓)
45	40, 8, 44	wsbc 3776	. . . 4 wff [(Itv‘𝑓) / 𝑖]∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)))
46		cbs 17140	. . . . 5 class Base
47	42, 46	cfv 6540	. . . 4 class (Base‘𝑓)
48	45, 31, 47	wsbc 3776	. . 3 wff [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖]∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)))
49	48, 41	cab 2710	. 2 class {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖]∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)))}
50	1, 49	wceq 1542	1 wff TarskiGE = {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖]∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)))}

This definition is referenced by:  istrkge  27688