Metamath Proof Explorer

Definition df-trkgcb

Description: Define the class of geometries fulfilling the five segment axiom, Axiom A5 of Schwabhauser p. 11, and segment construction axiom, Axiom A4 of Schwabhauser p. 11. (Contributed by Thierry Arnoux, 14-Mar-2019)

Ref Expression
Assertion df-trkgcb ⊢ 𝒢 Tarski CB = f | [˙Base f / p]˙ [˙ dist ⁡ f / d]˙ [˙ Itv ⁡ f / i]˙ ∀ x ∈ p ∀ y ∈ p ∀ z ∈ p ∀ u ∈ p ∀ a ∈ p ∀ b ∈ p ∀ c ∈ p ∀ v ∈ p x ≠ y ∧ y ∈ x i z ∧ b ∈ a i c ∧ x d y = a d b ∧ y d z = b d c ∧ x d u = a d v ∧ y d u = b d v → z d u = c d v ∧ ∀ x ∈ p ∀ y ∈ p ∀ a ∈ p ∀ b ∈ p ∃ z ∈ p y ∈ x i z ∧ y d z = a d b

Detailed syntax breakdown

Step Hyp Ref Expression
0 cstrkgcb class 𝒢 Tarski CB
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 cds class dist
7 3 6 cfv class dist ⁡ f
8 vd setvar d
9 citv class Itv
10 3 9 cfv class Itv ⁡ f
11 vi setvar i
12 vx setvar x
13 5 cv setvar p
14 vy setvar y
15 vz setvar z
16 vu setvar u
17 va setvar a
18 vb setvar b
19 vc setvar c
20 vv setvar v
21 12 cv setvar x
22 14 cv setvar y
23 21 22 wne wff x ≠ y
24 11 cv setvar i
25 15 cv setvar z
26 21 25 24 co class x i z
27 22 26 wcel wff y ∈ x i z
28 18 cv setvar b
29 17 cv setvar a
30 19 cv setvar c
31 29 30 24 co class a i c
32 28 31 wcel wff b ∈ a i c
33 23 27 32 w3a wff x ≠ y ∧ y ∈ x i z ∧ b ∈ a i c
34 8 cv setvar d
35 21 22 34 co class x d y
36 29 28 34 co class a d b
37 35 36 wceq wff x d y = a d b
38 22 25 34 co class y d z
39 28 30 34 co class b d c
40 38 39 wceq wff y d z = b d c
41 37 40 wa wff x d y = a d b ∧ y d z = b d c
42 16 cv setvar u
43 21 42 34 co class x d u
44 20 cv setvar v
45 29 44 34 co class a d v
46 43 45 wceq wff x d u = a d v
47 22 42 34 co class y d u
48 28 44 34 co class b d v
49 47 48 wceq wff y d u = b d v
50 46 49 wa wff x d u = a d v ∧ y d u = b d v
51 41 50 wa wff x d y = a d b ∧ y d z = b d c ∧ x d u = a d v ∧ y d u = b d v
52 33 51 wa wff x ≠ y ∧ y ∈ x i z ∧ b ∈ a i c ∧ x d y = a d b ∧ y d z = b d c ∧ x d u = a d v ∧ y d u = b d v
53 25 42 34 co class z d u
54 30 44 34 co class c d v
55 53 54 wceq wff z d u = c d v
56 52 55 wi wff x ≠ y ∧ y ∈ x i z ∧ b ∈ a i c ∧ x d y = a d b ∧ y d z = b d c ∧ x d u = a d v ∧ y d u = b d v → z d u = c d v
57 56 20 13 wral wff ∀ v ∈ p x ≠ y ∧ y ∈ x i z ∧ b ∈ a i c ∧ x d y = a d b ∧ y d z = b d c ∧ x d u = a d v ∧ y d u = b d v → z d u = c d v
58 57 19 13 wral wff ∀ c ∈ p ∀ v ∈ p x ≠ y ∧ y ∈ x i z ∧ b ∈ a i c ∧ x d y = a d b ∧ y d z = b d c ∧ x d u = a d v ∧ y d u = b d v → z d u = c d v
59 58 18 13 wral wff ∀ b ∈ p ∀ c ∈ p ∀ v ∈ p x ≠ y ∧ y ∈ x i z ∧ b ∈ a i c ∧ x d y = a d b ∧ y d z = b d c ∧ x d u = a d v ∧ y d u = b d v → z d u = c d v
60 59 17 13 wral wff ∀ a ∈ p ∀ b ∈ p ∀ c ∈ p ∀ v ∈ p x ≠ y ∧ y ∈ x i z ∧ b ∈ a i c ∧ x d y = a d b ∧ y d z = b d c ∧ x d u = a d v ∧ y d u = b d v → z d u = c d v
61 60 16 13 wral wff ∀ u ∈ p ∀ a ∈ p ∀ b ∈ p ∀ c ∈ p ∀ v ∈ p x ≠ y ∧ y ∈ x i z ∧ b ∈ a i c ∧ x d y = a d b ∧ y d z = b d c ∧ x d u = a d v ∧ y d u = b d v → z d u = c d v
62 61 15 13 wral wff ∀ z ∈ p ∀ u ∈ p ∀ a ∈ p ∀ b ∈ p ∀ c ∈ p ∀ v ∈ p x ≠ y ∧ y ∈ x i z ∧ b ∈ a i c ∧ x d y = a d b ∧ y d z = b d c ∧ x d u = a d v ∧ y d u = b d v → z d u = c d v
63 62 14 13 wral wff ∀ y ∈ p ∀ z ∈ p ∀ u ∈ p ∀ a ∈ p ∀ b ∈ p ∀ c ∈ p ∀ v ∈ p x ≠ y ∧ y ∈ x i z ∧ b ∈ a i c ∧ x d y = a d b ∧ y d z = b d c ∧ x d u = a d v ∧ y d u = b d v → z d u = c d v
64 63 12 13 wral wff ∀ x ∈ p ∀ y ∈ p ∀ z ∈ p ∀ u ∈ p ∀ a ∈ p ∀ b ∈ p ∀ c ∈ p ∀ v ∈ p x ≠ y ∧ y ∈ x i z ∧ b ∈ a i c ∧ x d y = a d b ∧ y d z = b d c ∧ x d u = a d v ∧ y d u = b d v → z d u = c d v
65 38 36 wceq wff y d z = a d b
66 27 65 wa wff y ∈ x i z ∧ y d z = a d b
67 66 15 13 wrex wff ∃ z ∈ p y ∈ x i z ∧ y d z = a d b
68 67 18 13 wral wff ∀ b ∈ p ∃ z ∈ p y ∈ x i z ∧ y d z = a d b
69 68 17 13 wral wff ∀ a ∈ p ∀ b ∈ p ∃ z ∈ p y ∈ x i z ∧ y d z = a d b
70 69 14 13 wral wff ∀ y ∈ p ∀ a ∈ p ∀ b ∈ p ∃ z ∈ p y ∈ x i z ∧ y d z = a d b
71 70 12 13 wral wff ∀ x ∈ p ∀ y ∈ p ∀ a ∈ p ∀ b ∈ p ∃ z ∈ p y ∈ x i z ∧ y d z = a d b
72 64 71 wa wff ∀ x ∈ p ∀ y ∈ p ∀ z ∈ p ∀ u ∈ p ∀ a ∈ p ∀ b ∈ p ∀ c ∈ p ∀ v ∈ p x ≠ y ∧ y ∈ x i z ∧ b ∈ a i c ∧ x d y = a d b ∧ y d z = b d c ∧ x d u = a d v ∧ y d u = b d v → z d u = c d v ∧ ∀ x ∈ p ∀ y ∈ p ∀ a ∈ p ∀ b ∈ p ∃ z ∈ p y ∈ x i z ∧ y d z = a d b
73 72 11 10 wsbc wff [˙ Itv ⁡ f / i]˙ ∀ x ∈ p ∀ y ∈ p ∀ z ∈ p ∀ u ∈ p ∀ a ∈ p ∀ b ∈ p ∀ c ∈ p ∀ v ∈ p x ≠ y ∧ y ∈ x i z ∧ b ∈ a i c ∧ x d y = a d b ∧ y d z = b d c ∧ x d u = a d v ∧ y d u = b d v → z d u = c d v ∧ ∀ x ∈ p ∀ y ∈ p ∀ a ∈ p ∀ b ∈ p ∃ z ∈ p y ∈ x i z ∧ y d z = a d b
74 73 8 7 wsbc wff [˙ dist ⁡ f / d]˙ [˙ Itv ⁡ f / i]˙ ∀ x ∈ p ∀ y ∈ p ∀ z ∈ p ∀ u ∈ p ∀ a ∈ p ∀ b ∈ p ∀ c ∈ p ∀ v ∈ p x ≠ y ∧ y ∈ x i z ∧ b ∈ a i c ∧ x d y = a d b ∧ y d z = b d c ∧ x d u = a d v ∧ y d u = b d v → z d u = c d v ∧ ∀ x ∈ p ∀ y ∈ p ∀ a ∈ p ∀ b ∈ p ∃ z ∈ p y ∈ x i z ∧ y d z = a d b
75 74 5 4 wsbc wff [˙Base f / p]˙ [˙ dist ⁡ f / d]˙ [˙ Itv ⁡ f / i]˙ ∀ x ∈ p ∀ y ∈ p ∀ z ∈ p ∀ u ∈ p ∀ a ∈ p ∀ b ∈ p ∀ c ∈ p ∀ v ∈ p x ≠ y ∧ y ∈ x i z ∧ b ∈ a i c ∧ x d y = a d b ∧ y d z = b d c ∧ x d u = a d v ∧ y d u = b d v → z d u = c d v ∧ ∀ x ∈ p ∀ y ∈ p ∀ a ∈ p ∀ b ∈ p ∃ z ∈ p y ∈ x i z ∧ y d z = a d b
76 75 1 cab class f | [˙Base f / p]˙ [˙ dist ⁡ f / d]˙ [˙ Itv ⁡ f / i]˙ ∀ x ∈ p ∀ y ∈ p ∀ z ∈ p ∀ u ∈ p ∀ a ∈ p ∀ b ∈ p ∀ c ∈ p ∀ v ∈ p x ≠ y ∧ y ∈ x i z ∧ b ∈ a i c ∧ x d y = a d b ∧ y d z = b d c ∧ x d u = a d v ∧ y d u = b d v → z d u = c d v ∧ ∀ x ∈ p ∀ y ∈ p ∀ a ∈ p ∀ b ∈ p ∃ z ∈ p y ∈ x i z ∧ y d z = a d b
77 0 76 wceq wff 𝒢 Tarski CB = f | [˙Base f / p]˙ [˙ dist ⁡ f / d]˙ [˙ Itv ⁡ f / i]˙ ∀ x ∈ p ∀ y ∈ p ∀ z ∈ p ∀ u ∈ p ∀ a ∈ p ∀ b ∈ p ∀ c ∈ p ∀ v ∈ p x ≠ y ∧ y ∈ x i z ∧ b ∈ a i c ∧ x d y = a d b ∧ y d z = b d c ∧ x d u = a d v ∧ y d u = b d v → z d u = c d v ∧ ∀ x ∈ p ∀ y ∈ p ∀ a ∈ p ∀ b ∈ p ∃ z ∈ p y ∈ x i z ∧ y d z = a d b