Theorem brafs

Description: Binary relation form of the outer five segment predicate. (Contributed by Scott Fenton, 21-Sep-2013)

	Ref	Expression
Hypotheses	brafs.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	brafs.d	⊢ − = ( dist ‘ 𝐺 )
	brafs.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	brafs.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	brafs.o	⊢ 𝑂 = ( AFS ‘ 𝐺 )
	brafs.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	brafs.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	brafs.3	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	brafs.4	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
	brafs.5	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
	brafs.6	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
	brafs.7	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
	brafs.8	⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
Assertion	brafs	⊢ ( 𝜑 → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ 𝑂 ⟨ ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑍 , 𝑊 ⟩ ⟩ ↔ ( ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ ( ( 𝐴 − 𝐵 ) = ( 𝑋 − 𝑌 ) ∧ ( 𝐵 − 𝐶 ) = ( 𝑌 − 𝑍 ) ) ∧ ( ( 𝐴 − 𝐷 ) = ( 𝑋 − 𝑊 ) ∧ ( 𝐵 − 𝐷 ) = ( 𝑌 − 𝑊 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		brafs.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		brafs.d	⊢ − = ( dist ‘ 𝐺 )
3		brafs.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		brafs.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		brafs.o	⊢ 𝑂 = ( AFS ‘ 𝐺 )
6		brafs.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7		brafs.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
8		brafs.3	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
9		brafs.4	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
10		brafs.5	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
11		brafs.6	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
12		brafs.7	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
13		brafs.8	⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
14		oveq1	⊢ ( 𝑎 = 𝐴 → ( 𝑎 𝐼 𝑐 ) = ( 𝐴 𝐼 𝑐 ) )
15	14	eleq2d	⊢ ( 𝑎 = 𝐴 → ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ↔ 𝑏 ∈ ( 𝐴 𝐼 𝑐 ) ) )
16	15	anbi1d	⊢ ( 𝑎 = 𝐴 → ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ↔ ( 𝑏 ∈ ( 𝐴 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) )
17		oveq1	⊢ ( 𝑎 = 𝐴 → ( 𝑎 − 𝑏 ) = ( 𝐴 − 𝑏 ) )
18	17	eqeq1d	⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ↔ ( 𝐴 − 𝑏 ) = ( 𝑥 − 𝑦 ) ) )
19	18	anbi1d	⊢ ( 𝑎 = 𝐴 → ( ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ↔ ( ( 𝐴 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ) )
20		oveq1	⊢ ( 𝑎 = 𝐴 → ( 𝑎 − 𝑑 ) = ( 𝐴 − 𝑑 ) )
21	20	eqeq1d	⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ↔ ( 𝐴 − 𝑑 ) = ( 𝑥 − 𝑤 ) ) )
22	21	anbi1d	⊢ ( 𝑎 = 𝐴 → ( ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ↔ ( ( 𝐴 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) )
23	16 19 22	3anbi123d	⊢ ( 𝑎 = 𝐴 → ( ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ↔ ( ( 𝑏 ∈ ( 𝐴 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝐴 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝐴 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) )
24		eleq1	⊢ ( 𝑏 = 𝐵 → ( 𝑏 ∈ ( 𝐴 𝐼 𝑐 ) ↔ 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ) )
25	24	anbi1d	⊢ ( 𝑏 = 𝐵 → ( ( 𝑏 ∈ ( 𝐴 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ↔ ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) )
26		oveq2	⊢ ( 𝑏 = 𝐵 → ( 𝐴 − 𝑏 ) = ( 𝐴 − 𝐵 ) )
27	26	eqeq1d	⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 − 𝑏 ) = ( 𝑥 − 𝑦 ) ↔ ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑦 ) ) )
28		oveq1	⊢ ( 𝑏 = 𝐵 → ( 𝑏 − 𝑐 ) = ( 𝐵 − 𝑐 ) )
29	28	eqeq1d	⊢ ( 𝑏 = 𝐵 → ( ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ↔ ( 𝐵 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) )
30	27 29	anbi12d	⊢ ( 𝑏 = 𝐵 → ( ( ( 𝐴 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ↔ ( ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ) )
31		oveq1	⊢ ( 𝑏 = 𝐵 → ( 𝑏 − 𝑑 ) = ( 𝐵 − 𝑑 ) )
32	31	eqeq1d	⊢ ( 𝑏 = 𝐵 → ( ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ↔ ( 𝐵 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) )
33	32	anbi2d	⊢ ( 𝑏 = 𝐵 → ( ( ( 𝐴 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ↔ ( ( 𝐴 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝐵 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) )
34	25 30 33	3anbi123d	⊢ ( 𝑏 = 𝐵 → ( ( ( 𝑏 ∈ ( 𝐴 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝐴 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝐴 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ↔ ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝐴 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝐵 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) )
35		oveq2	⊢ ( 𝑐 = 𝐶 → ( 𝐴 𝐼 𝑐 ) = ( 𝐴 𝐼 𝐶 ) )
36	35	eleq2d	⊢ ( 𝑐 = 𝐶 → ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ↔ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) )
37	36	anbi1d	⊢ ( 𝑐 = 𝐶 → ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ↔ ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) )
38		oveq2	⊢ ( 𝑐 = 𝐶 → ( 𝐵 − 𝑐 ) = ( 𝐵 − 𝐶 ) )
39	38	eqeq1d	⊢ ( 𝑐 = 𝐶 → ( ( 𝐵 − 𝑐 ) = ( 𝑦 − 𝑧 ) ↔ ( 𝐵 − 𝐶 ) = ( 𝑦 − 𝑧 ) ) )
40	39	anbi2d	⊢ ( 𝑐 = 𝐶 → ( ( ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ↔ ( ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝐵 − 𝐶 ) = ( 𝑦 − 𝑧 ) ) ) )
41	37 40	3anbi12d	⊢ ( 𝑐 = 𝐶 → ( ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝐴 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝐵 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ↔ ( ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝐵 − 𝐶 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝐴 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝐵 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) )
42		oveq2	⊢ ( 𝑑 = 𝐷 → ( 𝐴 − 𝑑 ) = ( 𝐴 − 𝐷 ) )
43	42	eqeq1d	⊢ ( 𝑑 = 𝐷 → ( ( 𝐴 − 𝑑 ) = ( 𝑥 − 𝑤 ) ↔ ( 𝐴 − 𝐷 ) = ( 𝑥 − 𝑤 ) ) )
44		oveq2	⊢ ( 𝑑 = 𝐷 → ( 𝐵 − 𝑑 ) = ( 𝐵 − 𝐷 ) )
45	44	eqeq1d	⊢ ( 𝑑 = 𝐷 → ( ( 𝐵 − 𝑑 ) = ( 𝑦 − 𝑤 ) ↔ ( 𝐵 − 𝐷 ) = ( 𝑦 − 𝑤 ) ) )
46	43 45	anbi12d	⊢ ( 𝑑 = 𝐷 → ( ( ( 𝐴 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝐵 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ↔ ( ( 𝐴 − 𝐷 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝐵 − 𝐷 ) = ( 𝑦 − 𝑤 ) ) ) )
47	46	3anbi3d	⊢ ( 𝑑 = 𝐷 → ( ( ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝐵 − 𝐶 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝐴 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝐵 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ↔ ( ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝐵 − 𝐶 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝐴 − 𝐷 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝐵 − 𝐷 ) = ( 𝑦 − 𝑤 ) ) ) ) )
48		oveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 𝐼 𝑧 ) = ( 𝑋 𝐼 𝑧 ) )
49	48	eleq2d	⊢ ( 𝑥 = 𝑋 → ( 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ↔ 𝑦 ∈ ( 𝑋 𝐼 𝑧 ) ) )
50	49	anbi2d	⊢ ( 𝑥 = 𝑋 → ( ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ↔ ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑧 ) ) ) )
51		oveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 − 𝑦 ) = ( 𝑋 − 𝑦 ) )
52	51	eqeq2d	⊢ ( 𝑥 = 𝑋 → ( ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑦 ) ↔ ( 𝐴 − 𝐵 ) = ( 𝑋 − 𝑦 ) ) )
53	52	anbi1d	⊢ ( 𝑥 = 𝑋 → ( ( ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝐵 − 𝐶 ) = ( 𝑦 − 𝑧 ) ) ↔ ( ( 𝐴 − 𝐵 ) = ( 𝑋 − 𝑦 ) ∧ ( 𝐵 − 𝐶 ) = ( 𝑦 − 𝑧 ) ) ) )
54		oveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 − 𝑤 ) = ( 𝑋 − 𝑤 ) )
55	54	eqeq2d	⊢ ( 𝑥 = 𝑋 → ( ( 𝐴 − 𝐷 ) = ( 𝑥 − 𝑤 ) ↔ ( 𝐴 − 𝐷 ) = ( 𝑋 − 𝑤 ) ) )
56	55	anbi1d	⊢ ( 𝑥 = 𝑋 → ( ( ( 𝐴 − 𝐷 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝐵 − 𝐷 ) = ( 𝑦 − 𝑤 ) ) ↔ ( ( 𝐴 − 𝐷 ) = ( 𝑋 − 𝑤 ) ∧ ( 𝐵 − 𝐷 ) = ( 𝑦 − 𝑤 ) ) ) )
57	50 53 56	3anbi123d	⊢ ( 𝑥 = 𝑋 → ( ( ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝐵 − 𝐶 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝐴 − 𝐷 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝐵 − 𝐷 ) = ( 𝑦 − 𝑤 ) ) ) ↔ ( ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑧 ) ) ∧ ( ( 𝐴 − 𝐵 ) = ( 𝑋 − 𝑦 ) ∧ ( 𝐵 − 𝐶 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝐴 − 𝐷 ) = ( 𝑋 − 𝑤 ) ∧ ( 𝐵 − 𝐷 ) = ( 𝑦 − 𝑤 ) ) ) ) )
58		eleq1	⊢ ( 𝑦 = 𝑌 → ( 𝑦 ∈ ( 𝑋 𝐼 𝑧 ) ↔ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) )
59	58	anbi2d	⊢ ( 𝑦 = 𝑌 → ( ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑧 ) ) ↔ ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ) )
60		oveq2	⊢ ( 𝑦 = 𝑌 → ( 𝑋 − 𝑦 ) = ( 𝑋 − 𝑌 ) )
61	60	eqeq2d	⊢ ( 𝑦 = 𝑌 → ( ( 𝐴 − 𝐵 ) = ( 𝑋 − 𝑦 ) ↔ ( 𝐴 − 𝐵 ) = ( 𝑋 − 𝑌 ) ) )
62		oveq1	⊢ ( 𝑦 = 𝑌 → ( 𝑦 − 𝑧 ) = ( 𝑌 − 𝑧 ) )
63	62	eqeq2d	⊢ ( 𝑦 = 𝑌 → ( ( 𝐵 − 𝐶 ) = ( 𝑦 − 𝑧 ) ↔ ( 𝐵 − 𝐶 ) = ( 𝑌 − 𝑧 ) ) )
64	61 63	anbi12d	⊢ ( 𝑦 = 𝑌 → ( ( ( 𝐴 − 𝐵 ) = ( 𝑋 − 𝑦 ) ∧ ( 𝐵 − 𝐶 ) = ( 𝑦 − 𝑧 ) ) ↔ ( ( 𝐴 − 𝐵 ) = ( 𝑋 − 𝑌 ) ∧ ( 𝐵 − 𝐶 ) = ( 𝑌 − 𝑧 ) ) ) )
65		oveq1	⊢ ( 𝑦 = 𝑌 → ( 𝑦 − 𝑤 ) = ( 𝑌 − 𝑤 ) )
66	65	eqeq2d	⊢ ( 𝑦 = 𝑌 → ( ( 𝐵 − 𝐷 ) = ( 𝑦 − 𝑤 ) ↔ ( 𝐵 − 𝐷 ) = ( 𝑌 − 𝑤 ) ) )
67	66	anbi2d	⊢ ( 𝑦 = 𝑌 → ( ( ( 𝐴 − 𝐷 ) = ( 𝑋 − 𝑤 ) ∧ ( 𝐵 − 𝐷 ) = ( 𝑦 − 𝑤 ) ) ↔ ( ( 𝐴 − 𝐷 ) = ( 𝑋 − 𝑤 ) ∧ ( 𝐵 − 𝐷 ) = ( 𝑌 − 𝑤 ) ) ) )
68	59 64 67	3anbi123d	⊢ ( 𝑦 = 𝑌 → ( ( ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑧 ) ) ∧ ( ( 𝐴 − 𝐵 ) = ( 𝑋 − 𝑦 ) ∧ ( 𝐵 − 𝐶 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝐴 − 𝐷 ) = ( 𝑋 − 𝑤 ) ∧ ( 𝐵 − 𝐷 ) = ( 𝑦 − 𝑤 ) ) ) ↔ ( ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ∧ ( ( 𝐴 − 𝐵 ) = ( 𝑋 − 𝑌 ) ∧ ( 𝐵 − 𝐶 ) = ( 𝑌 − 𝑧 ) ) ∧ ( ( 𝐴 − 𝐷 ) = ( 𝑋 − 𝑤 ) ∧ ( 𝐵 − 𝐷 ) = ( 𝑌 − 𝑤 ) ) ) ) )
69		oveq2	⊢ ( 𝑧 = 𝑍 → ( 𝑋 𝐼 𝑧 ) = ( 𝑋 𝐼 𝑍 ) )
70	69	eleq2d	⊢ ( 𝑧 = 𝑍 → ( 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ↔ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) )
71	70	anbi2d	⊢ ( 𝑧 = 𝑍 → ( ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ↔ ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) )
72		oveq2	⊢ ( 𝑧 = 𝑍 → ( 𝑌 − 𝑧 ) = ( 𝑌 − 𝑍 ) )
73	72	eqeq2d	⊢ ( 𝑧 = 𝑍 → ( ( 𝐵 − 𝐶 ) = ( 𝑌 − 𝑧 ) ↔ ( 𝐵 − 𝐶 ) = ( 𝑌 − 𝑍 ) ) )
74	73	anbi2d	⊢ ( 𝑧 = 𝑍 → ( ( ( 𝐴 − 𝐵 ) = ( 𝑋 − 𝑌 ) ∧ ( 𝐵 − 𝐶 ) = ( 𝑌 − 𝑧 ) ) ↔ ( ( 𝐴 − 𝐵 ) = ( 𝑋 − 𝑌 ) ∧ ( 𝐵 − 𝐶 ) = ( 𝑌 − 𝑍 ) ) ) )
75	71 74	3anbi12d	⊢ ( 𝑧 = 𝑍 → ( ( ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ∧ ( ( 𝐴 − 𝐵 ) = ( 𝑋 − 𝑌 ) ∧ ( 𝐵 − 𝐶 ) = ( 𝑌 − 𝑧 ) ) ∧ ( ( 𝐴 − 𝐷 ) = ( 𝑋 − 𝑤 ) ∧ ( 𝐵 − 𝐷 ) = ( 𝑌 − 𝑤 ) ) ) ↔ ( ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ ( ( 𝐴 − 𝐵 ) = ( 𝑋 − 𝑌 ) ∧ ( 𝐵 − 𝐶 ) = ( 𝑌 − 𝑍 ) ) ∧ ( ( 𝐴 − 𝐷 ) = ( 𝑋 − 𝑤 ) ∧ ( 𝐵 − 𝐷 ) = ( 𝑌 − 𝑤 ) ) ) ) )
76		oveq2	⊢ ( 𝑤 = 𝑊 → ( 𝑋 − 𝑤 ) = ( 𝑋 − 𝑊 ) )
77	76	eqeq2d	⊢ ( 𝑤 = 𝑊 → ( ( 𝐴 − 𝐷 ) = ( 𝑋 − 𝑤 ) ↔ ( 𝐴 − 𝐷 ) = ( 𝑋 − 𝑊 ) ) )
78		oveq2	⊢ ( 𝑤 = 𝑊 → ( 𝑌 − 𝑤 ) = ( 𝑌 − 𝑊 ) )
79	78	eqeq2d	⊢ ( 𝑤 = 𝑊 → ( ( 𝐵 − 𝐷 ) = ( 𝑌 − 𝑤 ) ↔ ( 𝐵 − 𝐷 ) = ( 𝑌 − 𝑊 ) ) )
80	77 79	anbi12d	⊢ ( 𝑤 = 𝑊 → ( ( ( 𝐴 − 𝐷 ) = ( 𝑋 − 𝑤 ) ∧ ( 𝐵 − 𝐷 ) = ( 𝑌 − 𝑤 ) ) ↔ ( ( 𝐴 − 𝐷 ) = ( 𝑋 − 𝑊 ) ∧ ( 𝐵 − 𝐷 ) = ( 𝑌 − 𝑊 ) ) ) )
81	80	3anbi3d	⊢ ( 𝑤 = 𝑊 → ( ( ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ ( ( 𝐴 − 𝐵 ) = ( 𝑋 − 𝑌 ) ∧ ( 𝐵 − 𝐶 ) = ( 𝑌 − 𝑍 ) ) ∧ ( ( 𝐴 − 𝐷 ) = ( 𝑋 − 𝑤 ) ∧ ( 𝐵 − 𝐷 ) = ( 𝑌 − 𝑤 ) ) ) ↔ ( ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ ( ( 𝐴 − 𝐵 ) = ( 𝑋 − 𝑌 ) ∧ ( 𝐵 − 𝐶 ) = ( 𝑌 − 𝑍 ) ) ∧ ( ( 𝐴 − 𝐷 ) = ( 𝑋 − 𝑊 ) ∧ ( 𝐵 − 𝐷 ) = ( 𝑌 − 𝑊 ) ) ) ) )
82	1 2 3 4	afsval	⊢ ( 𝜑 → ( AFS ‘ 𝐺 ) = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) } )
83	5 82	syl5eq	⊢ ( 𝜑 → 𝑂 = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) } )
84	23 34 41 47 57 68 75 81 83 6 7 8 9 10 11 12 13	br8d	⊢ ( 𝜑 → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ 𝑂 ⟨ ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑍 , 𝑊 ⟩ ⟩ ↔ ( ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ ( ( 𝐴 − 𝐵 ) = ( 𝑋 − 𝑌 ) ∧ ( 𝐵 − 𝐶 ) = ( 𝑌 − 𝑍 ) ) ∧ ( ( 𝐴 − 𝐷 ) = ( 𝑋 − 𝑊 ) ∧ ( 𝐵 − 𝐷 ) = ( 𝑌 − 𝑊 ) ) ) ) )