Definition 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	⊢ TarskiGB = { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑥 ) → 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝑖 𝑧 ) ) → ∃ 𝑎 ∈ 𝑝 ( 𝑎 ∈ ( 𝑢 𝑖 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝑖 𝑥 ) ) ) ∧ ∀ 𝑠 ∈ 𝒫 𝑝 ∀ 𝑡 ∈ 𝒫 𝑝 ( ∃ 𝑎 ∈ 𝑝 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝑖 𝑦 ) → ∃ 𝑏 ∈ 𝑝 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝑖 𝑦 ) ) ) }

Detailed syntax breakdown

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