Metamath Proof Explorer

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 ⊢ 𝒢 Tarski B = f | [˙Base f / p]˙ [˙ Itv ⁡ f / i]˙ ∀ x ∈ p ∀ y ∈ p y ∈ x i x → x = y ∧ ∀ x ∈ p ∀ y ∈ p ∀ z ∈ p ∀ u ∈ p ∀ v ∈ p u ∈ x i z ∧ v ∈ y i z → ∃ a ∈ p a ∈ u i y ∧ a ∈ v i x ∧ ∀ s ∈ 𝒫 p ∀ t ∈ 𝒫 p ∃ a ∈ p ∀ x ∈ s ∀ y ∈ t x ∈ a i y → ∃ b ∈ p ∀ x ∈ s ∀ y ∈ t b ∈ 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 ∈ x i x
17 13 12 wceq wff x = y
18 16 17 wi wff y ∈ x i x → x = y
19 18 11 10 wral wff ∀ y ∈ p y ∈ x i x → x = y
20 19 9 10 wral wff ∀ x ∈ p ∀ y ∈ p y ∈ x i x → 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 ∈ x i z
28 23 cv setvar v
29 12 25 14 co class y i z
30 28 29 wcel wff v ∈ y i z
31 27 30 wa wff u ∈ x i z ∧ v ∈ 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 ∈ u i y
36 28 13 14 co class v i x
37 33 36 wcel wff a ∈ v i x
38 35 37 wa wff a ∈ u i y ∧ a ∈ v i x
39 38 32 10 wrex wff ∃ a ∈ p a ∈ u i y ∧ a ∈ v i x
40 31 39 wi wff u ∈ x i z ∧ v ∈ y i z → ∃ a ∈ p a ∈ u i y ∧ a ∈ v i x
41 40 23 10 wral wff ∀ v ∈ p u ∈ x i z ∧ v ∈ y i z → ∃ a ∈ p a ∈ u i y ∧ a ∈ v i x
42 41 22 10 wral wff ∀ u ∈ p ∀ v ∈ p u ∈ x i z ∧ v ∈ y i z → ∃ a ∈ p a ∈ u i y ∧ a ∈ v i x
43 42 21 10 wral wff ∀ z ∈ p ∀ u ∈ p ∀ v ∈ p u ∈ x i z ∧ v ∈ y i z → ∃ a ∈ p a ∈ u i y ∧ a ∈ v i x
44 43 11 10 wral wff ∀ y ∈ p ∀ z ∈ p ∀ u ∈ p ∀ v ∈ p u ∈ x i z ∧ v ∈ y i z → ∃ a ∈ p a ∈ u i y ∧ a ∈ v i x
45 44 9 10 wral wff ∀ x ∈ p ∀ y ∈ p ∀ z ∈ p ∀ u ∈ p ∀ v ∈ p u ∈ x i z ∧ v ∈ y i z → ∃ a ∈ p a ∈ u i y ∧ a ∈ 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 ∈ a i y
53 52 11 50 wral wff ∀ y ∈ t x ∈ a i y
54 53 9 49 wral wff ∀ x ∈ s ∀ y ∈ t x ∈ a i y
55 54 32 10 wrex wff ∃ a ∈ p ∀ x ∈ s ∀ y ∈ t x ∈ 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 ∈ x i y
60 59 11 50 wral wff ∀ y ∈ t b ∈ x i y
61 60 9 49 wral wff ∀ x ∈ s ∀ y ∈ t b ∈ x i y
62 61 56 10 wrex wff ∃ b ∈ p ∀ x ∈ s ∀ y ∈ t b ∈ x i y
63 55 62 wi wff ∃ a ∈ p ∀ x ∈ s ∀ y ∈ t x ∈ a i y → ∃ b ∈ p ∀ x ∈ s ∀ y ∈ t b ∈ x i y
64 63 48 47 wral wff ∀ t ∈ 𝒫 p ∃ a ∈ p ∀ x ∈ s ∀ y ∈ t x ∈ a i y → ∃ b ∈ p ∀ x ∈ s ∀ y ∈ t b ∈ x i y
65 64 46 47 wral wff ∀ s ∈ 𝒫 p ∀ t ∈ 𝒫 p ∃ a ∈ p ∀ x ∈ s ∀ y ∈ t x ∈ a i y → ∃ b ∈ p ∀ x ∈ s ∀ y ∈ t b ∈ x i y
66 20 45 65 w3a wff ∀ x ∈ p ∀ y ∈ p y ∈ x i x → x = y ∧ ∀ x ∈ p ∀ y ∈ p ∀ z ∈ p ∀ u ∈ p ∀ v ∈ p u ∈ x i z ∧ v ∈ y i z → ∃ a ∈ p a ∈ u i y ∧ a ∈ v i x ∧ ∀ s ∈ 𝒫 p ∀ t ∈ 𝒫 p ∃ a ∈ p ∀ x ∈ s ∀ y ∈ t x ∈ a i y → ∃ b ∈ p ∀ x ∈ s ∀ y ∈ t b ∈ x i y
67 66 8 7 wsbc wff [˙ Itv ⁡ f / i]˙ ∀ x ∈ p ∀ y ∈ p y ∈ x i x → x = y ∧ ∀ x ∈ p ∀ y ∈ p ∀ z ∈ p ∀ u ∈ p ∀ v ∈ p u ∈ x i z ∧ v ∈ y i z → ∃ a ∈ p a ∈ u i y ∧ a ∈ v i x ∧ ∀ s ∈ 𝒫 p ∀ t ∈ 𝒫 p ∃ a ∈ p ∀ x ∈ s ∀ y ∈ t x ∈ a i y → ∃ b ∈ p ∀ x ∈ s ∀ y ∈ t b ∈ x i y
68 67 5 4 wsbc wff [˙Base f / p]˙ [˙ Itv ⁡ f / i]˙ ∀ x ∈ p ∀ y ∈ p y ∈ x i x → x = y ∧ ∀ x ∈ p ∀ y ∈ p ∀ z ∈ p ∀ u ∈ p ∀ v ∈ p u ∈ x i z ∧ v ∈ y i z → ∃ a ∈ p a ∈ u i y ∧ a ∈ v i x ∧ ∀ s ∈ 𝒫 p ∀ t ∈ 𝒫 p ∃ a ∈ p ∀ x ∈ s ∀ y ∈ t x ∈ a i y → ∃ b ∈ p ∀ x ∈ s ∀ y ∈ t b ∈ x i y
69 68 1 cab class f | [˙Base f / p]˙ [˙ Itv ⁡ f / i]˙ ∀ x ∈ p ∀ y ∈ p y ∈ x i x → x = y ∧ ∀ x ∈ p ∀ y ∈ p ∀ z ∈ p ∀ u ∈ p ∀ v ∈ p u ∈ x i z ∧ v ∈ y i z → ∃ a ∈ p a ∈ u i y ∧ a ∈ v i x ∧ ∀ s ∈ 𝒫 p ∀ t ∈ 𝒫 p ∃ a ∈ p ∀ x ∈ s ∀ y ∈ t x ∈ a i y → ∃ b ∈ p ∀ x ∈ s ∀ y ∈ t b ∈ x i y
70 0 69 wceq wff 𝒢 Tarski B = f | [˙Base f / p]˙ [˙ Itv ⁡ f / i]˙ ∀ x ∈ p ∀ y ∈ p y ∈ x i x → x = y ∧ ∀ x ∈ p ∀ y ∈ p ∀ z ∈ p ∀ u ∈ p ∀ v ∈ p u ∈ x i z ∧ v ∈ y i z → ∃ a ∈ p a ∈ u i y ∧ a ∈ v i x ∧ ∀ s ∈ 𝒫 p ∀ t ∈ 𝒫 p ∃ a ∈ p ∀ x ∈ s ∀ y ∈ t x ∈ a i y → ∃ b ∈ p ∀ x ∈ s ∀ y ∈ t b ∈ x i y