Definition df-afs

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

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

Detailed syntax breakdown

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