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 TarskiGCB = { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( dist ‘ 𝑓 ) / 𝑑 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑝 ∀ 𝑐 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( ( 𝑥 ≠ 𝑦 ∧ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( ( 𝑥 𝑑 𝑦 ) = ( 𝑎 𝑑 𝑏 ) ∧ ( 𝑦 𝑑 𝑧 ) = ( 𝑏 𝑑 𝑐 ) ) ∧ ( ( 𝑥 𝑑 𝑢 ) = ( 𝑎 𝑑 𝑣 ) ∧ ( 𝑦 𝑑 𝑢 ) = ( 𝑏 𝑑 𝑣 ) ) ) ) → ( 𝑧 𝑑 𝑢 ) = ( 𝑐 𝑑 𝑣 ) ) ∧ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ∧ ( 𝑦 𝑑 𝑧 ) = ( 𝑎 𝑑 𝑏 ) ) ) }

Detailed syntax breakdown

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