Definition df-afs 33620

Description: The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom (axtg5seg 27696). See df-ofs 34893. Definition 2.10 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 21-Sep-2013.) (Revised by Thierry Arnoux, 15-Mar-2019.)

Assertion

Ref	Expression
df-afs	⊢ AFS = (𝑔 ∈ TarskiG ↦ {⟨𝑒, 𝑓⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / ℎ][(Itv‘𝑔) / 𝑖]∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 ∃𝑐 ∈ 𝑝 ∃𝑑 ∈ 𝑝 ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ∃𝑤 ∈ 𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤))))})

Distinct variable group:   𝑎,𝑏,𝑐,𝑑,𝑥,𝑦,𝑧,𝑤,𝑒,𝑓,𝑔,ℎ,𝑖,𝑝

Detailed syntax breakdown of Definition df-afs

Step	Hyp	Ref	Expression
1		cafs 33619	. 2 class AFS
2		vg	. . 3 setvar 𝑔
3		cstrkg 27658	. . 3 class TarskiG
4		ve	. . . . . . . . . . . . . . . . . 18 setvar 𝑒
5	4	cv 1541	. . . . . . . . . . . . . . . . 17 class 𝑒
6		va	. . . . . . . . . . . . . . . . . . . 20 setvar 𝑎
7	6	cv 1541	. . . . . . . . . . . . . . . . . . 19 class 𝑎
8		vb	. . . . . . . . . . . . . . . . . . . 20 setvar 𝑏
9	8	cv 1541	. . . . . . . . . . . . . . . . . . 19 class 𝑏
10	7, 9	cop 4633	. . . . . . . . . . . . . . . . . 18 class ⟨𝑎, 𝑏⟩
11		vc	. . . . . . . . . . . . . . . . . . . 20 setvar 𝑐
12	11	cv 1541	. . . . . . . . . . . . . . . . . . 19 class 𝑐
13		vd	. . . . . . . . . . . . . . . . . . . 20 setvar 𝑑
14	13	cv 1541	. . . . . . . . . . . . . . . . . . 19 class 𝑑
15	12, 14	cop 4633	. . . . . . . . . . . . . . . . . 18 class ⟨𝑐, 𝑑⟩
16	10, 15	cop 4633	. . . . . . . . . . . . . . . . 17 class ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩
17	5, 16	wceq 1542	. . . . . . . . . . . . . . . 16 wff 𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩
18		vf	. . . . . . . . . . . . . . . . . 18 setvar 𝑓
19	18	cv 1541	. . . . . . . . . . . . . . . . 17 class 𝑓
20		vx	. . . . . . . . . . . . . . . . . . . 20 setvar 𝑥
21	20	cv 1541	. . . . . . . . . . . . . . . . . . 19 class 𝑥
22		vy	. . . . . . . . . . . . . . . . . . . 20 setvar 𝑦
23	22	cv 1541	. . . . . . . . . . . . . . . . . . 19 class 𝑦
24	21, 23	cop 4633	. . . . . . . . . . . . . . . . . 18 class ⟨𝑥, 𝑦⟩
25		vz	. . . . . . . . . . . . . . . . . . . 20 setvar 𝑧
26	25	cv 1541	. . . . . . . . . . . . . . . . . . 19 class 𝑧
27		vw	. . . . . . . . . . . . . . . . . . . 20 setvar 𝑤
28	27	cv 1541	. . . . . . . . . . . . . . . . . . 19 class 𝑤
29	26, 28	cop 4633	. . . . . . . . . . . . . . . . . 18 class ⟨𝑧, 𝑤⟩
30	24, 29	cop 4633	. . . . . . . . . . . . . . . . 17 class ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩
31	19, 30	wceq 1542	. . . . . . . . . . . . . . . 16 wff 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩
32		vi	. . . . . . . . . . . . . . . . . . . . 21 setvar 𝑖
33	32	cv 1541	. . . . . . . . . . . . . . . . . . . 20 class 𝑖
34	7, 12, 33	co 7404	. . . . . . . . . . . . . . . . . . 19 class (𝑎𝑖𝑐)
35	9, 34	wcel 2107	. . . . . . . . . . . . . . . . . 18 wff 𝑏 ∈ (𝑎𝑖𝑐)
36	21, 26, 33	co 7404	. . . . . . . . . . . . . . . . . . 19 class (𝑥𝑖𝑧)
37	23, 36	wcel 2107	. . . . . . . . . . . . . . . . . 18 wff 𝑦 ∈ (𝑥𝑖𝑧)
38	35, 37	wa 397	. . . . . . . . . . . . . . . . 17 wff (𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧))
39		vh	. . . . . . . . . . . . . . . . . . . . 21 setvar ℎ
40	39	cv 1541	. . . . . . . . . . . . . . . . . . . 20 class ℎ
41	7, 9, 40	co 7404	. . . . . . . . . . . . . . . . . . 19 class (𝑎ℎ𝑏)
42	21, 23, 40	co 7404	. . . . . . . . . . . . . . . . . . 19 class (𝑥ℎ𝑦)
43	41, 42	wceq 1542	. . . . . . . . . . . . . . . . . 18 wff (𝑎ℎ𝑏) = (𝑥ℎ𝑦)
44	9, 12, 40	co 7404	. . . . . . . . . . . . . . . . . . 19 class (𝑏ℎ𝑐)
45	23, 26, 40	co 7404	. . . . . . . . . . . . . . . . . . 19 class (𝑦ℎ𝑧)
46	44, 45	wceq 1542	. . . . . . . . . . . . . . . . . 18 wff (𝑏ℎ𝑐) = (𝑦ℎ𝑧)
47	43, 46	wa 397	. . . . . . . . . . . . . . . . 17 wff ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧))
48	7, 14, 40	co 7404	. . . . . . . . . . . . . . . . . . 19 class (𝑎ℎ𝑑)
49	21, 28, 40	co 7404	. . . . . . . . . . . . . . . . . . 19 class (𝑥ℎ𝑤)
50	48, 49	wceq 1542	. . . . . . . . . . . . . . . . . 18 wff (𝑎ℎ𝑑) = (𝑥ℎ𝑤)
51	9, 14, 40	co 7404	. . . . . . . . . . . . . . . . . . 19 class (𝑏ℎ𝑑)
52	23, 28, 40	co 7404	. . . . . . . . . . . . . . . . . . 19 class (𝑦ℎ𝑤)
53	51, 52	wceq 1542	. . . . . . . . . . . . . . . . . 18 wff (𝑏ℎ𝑑) = (𝑦ℎ𝑤)
54	50, 53	wa 397	. . . . . . . . . . . . . . . . 17 wff ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤))
55	38, 47, 54	w3a 1088	. . . . . . . . . . . . . . . 16 wff ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤)))
56	17, 31, 55	w3a 1088	. . . . . . . . . . . . . . 15 wff (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤))))
57		vp	. . . . . . . . . . . . . . . 16 setvar 𝑝
58	57	cv 1541	. . . . . . . . . . . . . . 15 class 𝑝
59	56, 27, 58	wrex 3071	. . . . . . . . . . . . . 14 wff ∃𝑤 ∈ 𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤))))
60	59, 25, 58	wrex 3071	. . . . . . . . . . . . 13 wff ∃𝑧 ∈ 𝑝 ∃𝑤 ∈ 𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤))))
61	60, 22, 58	wrex 3071	. . . . . . . . . . . 12 wff ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ∃𝑤 ∈ 𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤))))
62	61, 20, 58	wrex 3071	. . . . . . . . . . 11 wff ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ∃𝑤 ∈ 𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤))))
63	62, 13, 58	wrex 3071	. . . . . . . . . 10 wff ∃𝑑 ∈ 𝑝 ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ∃𝑤 ∈ 𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤))))
64	63, 11, 58	wrex 3071	. . . . . . . . 9 wff ∃𝑐 ∈ 𝑝 ∃𝑑 ∈ 𝑝 ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ∃𝑤 ∈ 𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤))))
65	64, 8, 58	wrex 3071	. . . . . . . 8 wff ∃𝑏 ∈ 𝑝 ∃𝑐 ∈ 𝑝 ∃𝑑 ∈ 𝑝 ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ∃𝑤 ∈ 𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤))))
66	65, 6, 58	wrex 3071	. . . . . . 7 wff ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 ∃𝑐 ∈ 𝑝 ∃𝑑 ∈ 𝑝 ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ∃𝑤 ∈ 𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤))))
67	2	cv 1541	. . . . . . . 8 class 𝑔
68		citv 27664	. . . . . . . 8 class Itv
69	67, 68	cfv 6540	. . . . . . 7 class (Itv‘𝑔)
70	66, 32, 69	wsbc 3776	. . . . . 6 wff [(Itv‘𝑔) / 𝑖]∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 ∃𝑐 ∈ 𝑝 ∃𝑑 ∈ 𝑝 ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ∃𝑤 ∈ 𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤))))
71		cds 17202	. . . . . . 7 class dist
72	67, 71	cfv 6540	. . . . . 6 class (dist‘𝑔)
73	70, 39, 72	wsbc 3776	. . . . 5 wff [(dist‘𝑔) / ℎ][(Itv‘𝑔) / 𝑖]∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 ∃𝑐 ∈ 𝑝 ∃𝑑 ∈ 𝑝 ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ∃𝑤 ∈ 𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤))))
74		cbs 17140	. . . . . 6 class Base
75	67, 74	cfv 6540	. . . . 5 class (Base‘𝑔)
76	73, 57, 75	wsbc 3776	. . . 4 wff [(Base‘𝑔) / 𝑝][(dist‘𝑔) / ℎ][(Itv‘𝑔) / 𝑖]∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 ∃𝑐 ∈ 𝑝 ∃𝑑 ∈ 𝑝 ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ∃𝑤 ∈ 𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤))))
77	76, 4, 18	copab 5209	. . 3 class {⟨𝑒, 𝑓⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / ℎ][(Itv‘𝑔) / 𝑖]∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 ∃𝑐 ∈ 𝑝 ∃𝑑 ∈ 𝑝 ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ∃𝑤 ∈ 𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤))))}
78	2, 3, 77	cmpt 5230	. 2 class (𝑔 ∈ TarskiG ↦ {⟨𝑒, 𝑓⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / ℎ][(Itv‘𝑔) / 𝑖]∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 ∃𝑐 ∈ 𝑝 ∃𝑑 ∈ 𝑝 ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ∃𝑤 ∈ 𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤))))})
79	1, 78	wceq 1542	1 wff AFS = (𝑔 ∈ TarskiG ↦ {⟨𝑒, 𝑓⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / ℎ][(Itv‘𝑔) / 𝑖]∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 ∃𝑐 ∈ 𝑝 ∃𝑑 ∈ 𝑝 ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ∃𝑤 ∈ 𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤))))})

This definition is referenced by:  afsval  33621