Theorem brafs

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

	Ref	Expression
Hypotheses	brafs.p	$$⊢P={\mathrm{Base}}_G$$
	brafs.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	brafs.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	brafs.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	brafs.o	$$⊢O=AFS\left(G\right)$$
	brafs.1	$$⊢\phi \to A\in P$$
	brafs.2	$$⊢\phi \to B\in P$$
	brafs.3	$$⊢\phi \to C\in P$$
	brafs.4	$$⊢\phi \to D\in P$$
	brafs.5	$$⊢\phi \to X\in P$$
	brafs.6	$$⊢\phi \to Y\in P$$
	brafs.7	$$⊢\phi \to Z\in P$$
	brafs.8	$$⊢\phi \to W\in P$$
Assertion	brafs	$$⊢\phi \to \left(⟨⟨A,B⟩,⟨C,D⟩⟩O⟨⟨X,Y⟩,⟨Z,W⟩⟩\leftrightarrow \left(\left(B\in \left(AIC\right)\wedge Y\in \left(XIZ\right)\right)\wedge \left(A\underset{\dot{}}{-}B=X\underset{\dot{}}{-}Y\wedge B\underset{\dot{}}{-}C=Y\underset{\dot{}}{-}Z\right)\wedge \left(A\underset{\dot{}}{-}D=X\underset{\dot{}}{-}W\wedge B\underset{\dot{}}{-}D=Y\underset{\dot{}}{-}W\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		brafs.p	$$⊢P={\mathrm{Base}}_G$$
2		brafs.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		brafs.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		brafs.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
5		brafs.o	$$⊢O=AFS\left(G\right)$$
6		brafs.1	$$⊢\phi \to A\in P$$
7		brafs.2	$$⊢\phi \to B\in P$$
8		brafs.3	$$⊢\phi \to C\in P$$
9		brafs.4	$$⊢\phi \to D\in P$$
10		brafs.5	$$⊢\phi \to X\in P$$
11		brafs.6	$$⊢\phi \to Y\in P$$
12		brafs.7	$$⊢\phi \to Z\in P$$
13		brafs.8	$$⊢\phi \to W\in P$$
14		oveq1	$$⊢a=A\to aIc=AIc$$
15	14	eleq2d	$$⊢a=A\to \left(b\in \left(aIc\right)\leftrightarrow b\in \left(AIc\right)\right)$$
16	15	anbi1d	$$⊢a=A\to \left(\left(b\in \left(aIc\right)\wedge y\in \left(xIz\right)\right)\leftrightarrow \left(b\in \left(AIc\right)\wedge y\in \left(xIz\right)\right)\right)$$
17		oveq1	$$⊢a=A\to a\underset{\dot{}}{-}b=A\underset{\dot{}}{-}b$$
18	17	eqeq1d	$$⊢a=A\to \left(a\underset{\dot{}}{-}b=x\underset{\dot{}}{-}y\leftrightarrow A\underset{\dot{}}{-}b=x\underset{\dot{}}{-}y\right)$$
19	18	anbi1d	$$⊢a=A\to \left(\left(a\underset{\dot{}}{-}b=x\underset{\dot{}}{-}y\wedge b\underset{\dot{}}{-}c=y\underset{\dot{}}{-}z\right)\leftrightarrow \left(A\underset{\dot{}}{-}b=x\underset{\dot{}}{-}y\wedge b\underset{\dot{}}{-}c=y\underset{\dot{}}{-}z\right)\right)$$
20		oveq1	$$⊢a=A\to a\underset{\dot{}}{-}d=A\underset{\dot{}}{-}d$$
21	20	eqeq1d	$$⊢a=A\to \left(a\underset{\dot{}}{-}d=x\underset{\dot{}}{-}w\leftrightarrow A\underset{\dot{}}{-}d=x\underset{\dot{}}{-}w\right)$$
22	21	anbi1d	$$⊢a=A\to \left(\left(a\underset{\dot{}}{-}d=x\underset{\dot{}}{-}w\wedge b\underset{\dot{}}{-}d=y\underset{\dot{}}{-}w\right)\leftrightarrow \left(A\underset{\dot{}}{-}d=x\underset{\dot{}}{-}w\wedge b\underset{\dot{}}{-}d=y\underset{\dot{}}{-}w\right)\right)$$
23	16 19 22	3anbi123d	$$⊢a=A\to \left(\left(\left(b\in \left(aIc\right)\wedge y\in \left(xIz\right)\right)\wedge \left(a\underset{\dot{}}{-}b=x\underset{\dot{}}{-}y\wedge b\underset{\dot{}}{-}c=y\underset{\dot{}}{-}z\right)\wedge \left(a\underset{\dot{}}{-}d=x\underset{\dot{}}{-}w\wedge b\underset{\dot{}}{-}d=y\underset{\dot{}}{-}w\right)\right)\leftrightarrow \left(\left(b\in \left(AIc\right)\wedge y\in \left(xIz\right)\right)\wedge \left(A\underset{\dot{}}{-}b=x\underset{\dot{}}{-}y\wedge b\underset{\dot{}}{-}c=y\underset{\dot{}}{-}z\right)\wedge \left(A\underset{\dot{}}{-}d=x\underset{\dot{}}{-}w\wedge b\underset{\dot{}}{-}d=y\underset{\dot{}}{-}w\right)\right)\right)$$
24		eleq1	$$⊢b=B\to \left(b\in \left(AIc\right)\leftrightarrow B\in \left(AIc\right)\right)$$
25	24	anbi1d	$$⊢b=B\to \left(\left(b\in \left(AIc\right)\wedge y\in \left(xIz\right)\right)\leftrightarrow \left(B\in \left(AIc\right)\wedge y\in \left(xIz\right)\right)\right)$$
26		oveq2	$$⊢b=B\to A\underset{\dot{}}{-}b=A\underset{\dot{}}{-}B$$
27	26	eqeq1d	$$⊢b=B\to \left(A\underset{\dot{}}{-}b=x\underset{\dot{}}{-}y\leftrightarrow A\underset{\dot{}}{-}B=x\underset{\dot{}}{-}y\right)$$
28		oveq1	$$⊢b=B\to b\underset{\dot{}}{-}c=B\underset{\dot{}}{-}c$$
29	28	eqeq1d	$$⊢b=B\to \left(b\underset{\dot{}}{-}c=y\underset{\dot{}}{-}z\leftrightarrow B\underset{\dot{}}{-}c=y\underset{\dot{}}{-}z\right)$$
30	27 29	anbi12d	$$⊢b=B\to \left(\left(A\underset{\dot{}}{-}b=x\underset{\dot{}}{-}y\wedge b\underset{\dot{}}{-}c=y\underset{\dot{}}{-}z\right)\leftrightarrow \left(A\underset{\dot{}}{-}B=x\underset{\dot{}}{-}y\wedge B\underset{\dot{}}{-}c=y\underset{\dot{}}{-}z\right)\right)$$
31		oveq1	$$⊢b=B\to b\underset{\dot{}}{-}d=B\underset{\dot{}}{-}d$$
32	31	eqeq1d	$$⊢b=B\to \left(b\underset{\dot{}}{-}d=y\underset{\dot{}}{-}w\leftrightarrow B\underset{\dot{}}{-}d=y\underset{\dot{}}{-}w\right)$$
33	32	anbi2d	$$⊢b=B\to \left(\left(A\underset{\dot{}}{-}d=x\underset{\dot{}}{-}w\wedge b\underset{\dot{}}{-}d=y\underset{\dot{}}{-}w\right)\leftrightarrow \left(A\underset{\dot{}}{-}d=x\underset{\dot{}}{-}w\wedge B\underset{\dot{}}{-}d=y\underset{\dot{}}{-}w\right)\right)$$
34	25 30 33	3anbi123d	$$⊢b=B\to \left(\left(\left(b\in \left(AIc\right)\wedge y\in \left(xIz\right)\right)\wedge \left(A\underset{\dot{}}{-}b=x\underset{\dot{}}{-}y\wedge b\underset{\dot{}}{-}c=y\underset{\dot{}}{-}z\right)\wedge \left(A\underset{\dot{}}{-}d=x\underset{\dot{}}{-}w\wedge b\underset{\dot{}}{-}d=y\underset{\dot{}}{-}w\right)\right)\leftrightarrow \left(\left(B\in \left(AIc\right)\wedge y\in \left(xIz\right)\right)\wedge \left(A\underset{\dot{}}{-}B=x\underset{\dot{}}{-}y\wedge B\underset{\dot{}}{-}c=y\underset{\dot{}}{-}z\right)\wedge \left(A\underset{\dot{}}{-}d=x\underset{\dot{}}{-}w\wedge B\underset{\dot{}}{-}d=y\underset{\dot{}}{-}w\right)\right)\right)$$
35		oveq2	$$⊢c=C\to AIc=AIC$$
36	35	eleq2d	$$⊢c=C\to \left(B\in \left(AIc\right)\leftrightarrow B\in \left(AIC\right)\right)$$
37	36	anbi1d	$$⊢c=C\to \left(\left(B\in \left(AIc\right)\wedge y\in \left(xIz\right)\right)\leftrightarrow \left(B\in \left(AIC\right)\wedge y\in \left(xIz\right)\right)\right)$$
38		oveq2	$$⊢c=C\to B\underset{\dot{}}{-}c=B\underset{\dot{}}{-}C$$
39	38	eqeq1d	$$⊢c=C\to \left(B\underset{\dot{}}{-}c=y\underset{\dot{}}{-}z\leftrightarrow B\underset{\dot{}}{-}C=y\underset{\dot{}}{-}z\right)$$
40	39	anbi2d	$$⊢c=C\to \left(\left(A\underset{\dot{}}{-}B=x\underset{\dot{}}{-}y\wedge B\underset{\dot{}}{-}c=y\underset{\dot{}}{-}z\right)\leftrightarrow \left(A\underset{\dot{}}{-}B=x\underset{\dot{}}{-}y\wedge B\underset{\dot{}}{-}C=y\underset{\dot{}}{-}z\right)\right)$$
41	37 40	3anbi12d	$$⊢c=C\to \left(\left(\left(B\in \left(AIc\right)\wedge y\in \left(xIz\right)\right)\wedge \left(A\underset{\dot{}}{-}B=x\underset{\dot{}}{-}y\wedge B\underset{\dot{}}{-}c=y\underset{\dot{}}{-}z\right)\wedge \left(A\underset{\dot{}}{-}d=x\underset{\dot{}}{-}w\wedge B\underset{\dot{}}{-}d=y\underset{\dot{}}{-}w\right)\right)\leftrightarrow \left(\left(B\in \left(AIC\right)\wedge y\in \left(xIz\right)\right)\wedge \left(A\underset{\dot{}}{-}B=x\underset{\dot{}}{-}y\wedge B\underset{\dot{}}{-}C=y\underset{\dot{}}{-}z\right)\wedge \left(A\underset{\dot{}}{-}d=x\underset{\dot{}}{-}w\wedge B\underset{\dot{}}{-}d=y\underset{\dot{}}{-}w\right)\right)\right)$$
42		oveq2	$$⊢d=D\to A\underset{\dot{}}{-}d=A\underset{\dot{}}{-}D$$
43	42	eqeq1d	$$⊢d=D\to \left(A\underset{\dot{}}{-}d=x\underset{\dot{}}{-}w\leftrightarrow A\underset{\dot{}}{-}D=x\underset{\dot{}}{-}w\right)$$
44		oveq2	$$⊢d=D\to B\underset{\dot{}}{-}d=B\underset{\dot{}}{-}D$$
45	44	eqeq1d	$$⊢d=D\to \left(B\underset{\dot{}}{-}d=y\underset{\dot{}}{-}w\leftrightarrow B\underset{\dot{}}{-}D=y\underset{\dot{}}{-}w\right)$$
46	43 45	anbi12d	$$⊢d=D\to \left(\left(A\underset{\dot{}}{-}d=x\underset{\dot{}}{-}w\wedge B\underset{\dot{}}{-}d=y\underset{\dot{}}{-}w\right)\leftrightarrow \left(A\underset{\dot{}}{-}D=x\underset{\dot{}}{-}w\wedge B\underset{\dot{}}{-}D=y\underset{\dot{}}{-}w\right)\right)$$
47	46	3anbi3d	$$⊢d=D\to \left(\left(\left(B\in \left(AIC\right)\wedge y\in \left(xIz\right)\right)\wedge \left(A\underset{\dot{}}{-}B=x\underset{\dot{}}{-}y\wedge B\underset{\dot{}}{-}C=y\underset{\dot{}}{-}z\right)\wedge \left(A\underset{\dot{}}{-}d=x\underset{\dot{}}{-}w\wedge B\underset{\dot{}}{-}d=y\underset{\dot{}}{-}w\right)\right)\leftrightarrow \left(\left(B\in \left(AIC\right)\wedge y\in \left(xIz\right)\right)\wedge \left(A\underset{\dot{}}{-}B=x\underset{\dot{}}{-}y\wedge B\underset{\dot{}}{-}C=y\underset{\dot{}}{-}z\right)\wedge \left(A\underset{\dot{}}{-}D=x\underset{\dot{}}{-}w\wedge B\underset{\dot{}}{-}D=y\underset{\dot{}}{-}w\right)\right)\right)$$
48		oveq1	$$⊢x=X\to xIz=XIz$$
49	48	eleq2d	$$⊢x=X\to \left(y\in \left(xIz\right)\leftrightarrow y\in \left(XIz\right)\right)$$
50	49	anbi2d	$$⊢x=X\to \left(\left(B\in \left(AIC\right)\wedge y\in \left(xIz\right)\right)\leftrightarrow \left(B\in \left(AIC\right)\wedge y\in \left(XIz\right)\right)\right)$$
51		oveq1	$$⊢x=X\to x\underset{\dot{}}{-}y=X\underset{\dot{}}{-}y$$
52	51	eqeq2d	$$⊢x=X\to \left(A\underset{\dot{}}{-}B=x\underset{\dot{}}{-}y\leftrightarrow A\underset{\dot{}}{-}B=X\underset{\dot{}}{-}y\right)$$
53	52	anbi1d	$$⊢x=X\to \left(\left(A\underset{\dot{}}{-}B=x\underset{\dot{}}{-}y\wedge B\underset{\dot{}}{-}C=y\underset{\dot{}}{-}z\right)\leftrightarrow \left(A\underset{\dot{}}{-}B=X\underset{\dot{}}{-}y\wedge B\underset{\dot{}}{-}C=y\underset{\dot{}}{-}z\right)\right)$$
54		oveq1	$$⊢x=X\to x\underset{\dot{}}{-}w=X\underset{\dot{}}{-}w$$
55	54	eqeq2d	$$⊢x=X\to \left(A\underset{\dot{}}{-}D=x\underset{\dot{}}{-}w\leftrightarrow A\underset{\dot{}}{-}D=X\underset{\dot{}}{-}w\right)$$
56	55	anbi1d	$$⊢x=X\to \left(\left(A\underset{\dot{}}{-}D=x\underset{\dot{}}{-}w\wedge B\underset{\dot{}}{-}D=y\underset{\dot{}}{-}w\right)\leftrightarrow \left(A\underset{\dot{}}{-}D=X\underset{\dot{}}{-}w\wedge B\underset{\dot{}}{-}D=y\underset{\dot{}}{-}w\right)\right)$$
57	50 53 56	3anbi123d	$$⊢x=X\to \left(\left(\left(B\in \left(AIC\right)\wedge y\in \left(xIz\right)\right)\wedge \left(A\underset{\dot{}}{-}B=x\underset{\dot{}}{-}y\wedge B\underset{\dot{}}{-}C=y\underset{\dot{}}{-}z\right)\wedge \left(A\underset{\dot{}}{-}D=x\underset{\dot{}}{-}w\wedge B\underset{\dot{}}{-}D=y\underset{\dot{}}{-}w\right)\right)\leftrightarrow \left(\left(B\in \left(AIC\right)\wedge y\in \left(XIz\right)\right)\wedge \left(A\underset{\dot{}}{-}B=X\underset{\dot{}}{-}y\wedge B\underset{\dot{}}{-}C=y\underset{\dot{}}{-}z\right)\wedge \left(A\underset{\dot{}}{-}D=X\underset{\dot{}}{-}w\wedge B\underset{\dot{}}{-}D=y\underset{\dot{}}{-}w\right)\right)\right)$$
58		eleq1	$$⊢y=Y\to \left(y\in \left(XIz\right)\leftrightarrow Y\in \left(XIz\right)\right)$$
59	58	anbi2d	$$⊢y=Y\to \left(\left(B\in \left(AIC\right)\wedge y\in \left(XIz\right)\right)\leftrightarrow \left(B\in \left(AIC\right)\wedge Y\in \left(XIz\right)\right)\right)$$
60		oveq2	$$⊢y=Y\to X\underset{\dot{}}{-}y=X\underset{\dot{}}{-}Y$$
61	60	eqeq2d	$$⊢y=Y\to \left(A\underset{\dot{}}{-}B=X\underset{\dot{}}{-}y\leftrightarrow A\underset{\dot{}}{-}B=X\underset{\dot{}}{-}Y\right)$$
62		oveq1	$$⊢y=Y\to y\underset{\dot{}}{-}z=Y\underset{\dot{}}{-}z$$
63	62	eqeq2d	$$⊢y=Y\to \left(B\underset{\dot{}}{-}C=y\underset{\dot{}}{-}z\leftrightarrow B\underset{\dot{}}{-}C=Y\underset{\dot{}}{-}z\right)$$
64	61 63	anbi12d	$$⊢y=Y\to \left(\left(A\underset{\dot{}}{-}B=X\underset{\dot{}}{-}y\wedge B\underset{\dot{}}{-}C=y\underset{\dot{}}{-}z\right)\leftrightarrow \left(A\underset{\dot{}}{-}B=X\underset{\dot{}}{-}Y\wedge B\underset{\dot{}}{-}C=Y\underset{\dot{}}{-}z\right)\right)$$
65		oveq1	$$⊢y=Y\to y\underset{\dot{}}{-}w=Y\underset{\dot{}}{-}w$$
66	65	eqeq2d	$$⊢y=Y\to \left(B\underset{\dot{}}{-}D=y\underset{\dot{}}{-}w\leftrightarrow B\underset{\dot{}}{-}D=Y\underset{\dot{}}{-}w\right)$$
67	66	anbi2d	$$⊢y=Y\to \left(\left(A\underset{\dot{}}{-}D=X\underset{\dot{}}{-}w\wedge B\underset{\dot{}}{-}D=y\underset{\dot{}}{-}w\right)\leftrightarrow \left(A\underset{\dot{}}{-}D=X\underset{\dot{}}{-}w\wedge B\underset{\dot{}}{-}D=Y\underset{\dot{}}{-}w\right)\right)$$
68	59 64 67	3anbi123d	$$⊢y=Y\to \left(\left(\left(B\in \left(AIC\right)\wedge y\in \left(XIz\right)\right)\wedge \left(A\underset{\dot{}}{-}B=X\underset{\dot{}}{-}y\wedge B\underset{\dot{}}{-}C=y\underset{\dot{}}{-}z\right)\wedge \left(A\underset{\dot{}}{-}D=X\underset{\dot{}}{-}w\wedge B\underset{\dot{}}{-}D=y\underset{\dot{}}{-}w\right)\right)\leftrightarrow \left(\left(B\in \left(AIC\right)\wedge Y\in \left(XIz\right)\right)\wedge \left(A\underset{\dot{}}{-}B=X\underset{\dot{}}{-}Y\wedge B\underset{\dot{}}{-}C=Y\underset{\dot{}}{-}z\right)\wedge \left(A\underset{\dot{}}{-}D=X\underset{\dot{}}{-}w\wedge B\underset{\dot{}}{-}D=Y\underset{\dot{}}{-}w\right)\right)\right)$$
69		oveq2	$$⊢z=Z\to XIz=XIZ$$
70	69	eleq2d	$$⊢z=Z\to \left(Y\in \left(XIz\right)\leftrightarrow Y\in \left(XIZ\right)\right)$$
71	70	anbi2d	$$⊢z=Z\to \left(\left(B\in \left(AIC\right)\wedge Y\in \left(XIz\right)\right)\leftrightarrow \left(B\in \left(AIC\right)\wedge Y\in \left(XIZ\right)\right)\right)$$
72		oveq2	$$⊢z=Z\to Y\underset{\dot{}}{-}z=Y\underset{\dot{}}{-}Z$$
73	72	eqeq2d	$$⊢z=Z\to \left(B\underset{\dot{}}{-}C=Y\underset{\dot{}}{-}z\leftrightarrow B\underset{\dot{}}{-}C=Y\underset{\dot{}}{-}Z\right)$$
74	73	anbi2d	$$⊢z=Z\to \left(\left(A\underset{\dot{}}{-}B=X\underset{\dot{}}{-}Y\wedge B\underset{\dot{}}{-}C=Y\underset{\dot{}}{-}z\right)\leftrightarrow \left(A\underset{\dot{}}{-}B=X\underset{\dot{}}{-}Y\wedge B\underset{\dot{}}{-}C=Y\underset{\dot{}}{-}Z\right)\right)$$
75	71 74	3anbi12d	$$⊢z=Z\to \left(\left(\left(B\in \left(AIC\right)\wedge Y\in \left(XIz\right)\right)\wedge \left(A\underset{\dot{}}{-}B=X\underset{\dot{}}{-}Y\wedge B\underset{\dot{}}{-}C=Y\underset{\dot{}}{-}z\right)\wedge \left(A\underset{\dot{}}{-}D=X\underset{\dot{}}{-}w\wedge B\underset{\dot{}}{-}D=Y\underset{\dot{}}{-}w\right)\right)\leftrightarrow \left(\left(B\in \left(AIC\right)\wedge Y\in \left(XIZ\right)\right)\wedge \left(A\underset{\dot{}}{-}B=X\underset{\dot{}}{-}Y\wedge B\underset{\dot{}}{-}C=Y\underset{\dot{}}{-}Z\right)\wedge \left(A\underset{\dot{}}{-}D=X\underset{\dot{}}{-}w\wedge B\underset{\dot{}}{-}D=Y\underset{\dot{}}{-}w\right)\right)\right)$$
76		oveq2	$$⊢w=W\to X\underset{\dot{}}{-}w=X\underset{\dot{}}{-}W$$
77	76	eqeq2d	$$⊢w=W\to \left(A\underset{\dot{}}{-}D=X\underset{\dot{}}{-}w\leftrightarrow A\underset{\dot{}}{-}D=X\underset{\dot{}}{-}W\right)$$
78		oveq2	$$⊢w=W\to Y\underset{\dot{}}{-}w=Y\underset{\dot{}}{-}W$$
79	78	eqeq2d	$$⊢w=W\to \left(B\underset{\dot{}}{-}D=Y\underset{\dot{}}{-}w\leftrightarrow B\underset{\dot{}}{-}D=Y\underset{\dot{}}{-}W\right)$$
80	77 79	anbi12d	$$⊢w=W\to \left(\left(A\underset{\dot{}}{-}D=X\underset{\dot{}}{-}w\wedge B\underset{\dot{}}{-}D=Y\underset{\dot{}}{-}w\right)\leftrightarrow \left(A\underset{\dot{}}{-}D=X\underset{\dot{}}{-}W\wedge B\underset{\dot{}}{-}D=Y\underset{\dot{}}{-}W\right)\right)$$
81	80	3anbi3d	$$⊢w=W\to \left(\left(\left(B\in \left(AIC\right)\wedge Y\in \left(XIZ\right)\right)\wedge \left(A\underset{\dot{}}{-}B=X\underset{\dot{}}{-}Y\wedge B\underset{\dot{}}{-}C=Y\underset{\dot{}}{-}Z\right)\wedge \left(A\underset{\dot{}}{-}D=X\underset{\dot{}}{-}w\wedge B\underset{\dot{}}{-}D=Y\underset{\dot{}}{-}w\right)\right)\leftrightarrow \left(\left(B\in \left(AIC\right)\wedge Y\in \left(XIZ\right)\right)\wedge \left(A\underset{\dot{}}{-}B=X\underset{\dot{}}{-}Y\wedge B\underset{\dot{}}{-}C=Y\underset{\dot{}}{-}Z\right)\wedge \left(A\underset{\dot{}}{-}D=X\underset{\dot{}}{-}W\wedge B\underset{\dot{}}{-}D=Y\underset{\dot{}}{-}W\right)\right)\right)$$
82	1 2 3 4	afsval	$$⊢\phi \to AFS\left(G\right)=\left\{⟨e,f⟩|\exists a\in P\exists b\in P\exists c\in P\exists d\in P\exists x\in P\exists y\in P\exists z\in P\exists w\in P\left(e=⟨⟨a,b⟩,⟨c,d⟩⟩\wedge f=⟨⟨x,y⟩,⟨z,w⟩⟩\wedge \left(\left(b\in \left(aIc\right)\wedge y\in \left(xIz\right)\right)\wedge \left(a\underset{\dot{}}{-}b=x\underset{\dot{}}{-}y\wedge b\underset{\dot{}}{-}c=y\underset{\dot{}}{-}z\right)\wedge \left(a\underset{\dot{}}{-}d=x\underset{\dot{}}{-}w\wedge b\underset{\dot{}}{-}d=y\underset{\dot{}}{-}w\right)\right)\right)\right\}$$
83	5 82	syl5eq	$$⊢\phi \to O=\left\{⟨e,f⟩|\exists a\in P\exists b\in P\exists c\in P\exists d\in P\exists x\in P\exists y\in P\exists z\in P\exists w\in P\left(e=⟨⟨a,b⟩,⟨c,d⟩⟩\wedge f=⟨⟨x,y⟩,⟨z,w⟩⟩\wedge \left(\left(b\in \left(aIc\right)\wedge y\in \left(xIz\right)\right)\wedge \left(a\underset{\dot{}}{-}b=x\underset{\dot{}}{-}y\wedge b\underset{\dot{}}{-}c=y\underset{\dot{}}{-}z\right)\wedge \left(a\underset{\dot{}}{-}d=x\underset{\dot{}}{-}w\wedge b\underset{\dot{}}{-}d=y\underset{\dot{}}{-}w\right)\right)\right)\right\}$$
84	23 34 41 47 57 68 75 81 83 6 7 8 9 10 11 12 13	br8d	$$⊢\phi \to \left(⟨⟨A,B⟩,⟨C,D⟩⟩O⟨⟨X,Y⟩,⟨Z,W⟩⟩\leftrightarrow \left(\left(B\in \left(AIC\right)\wedge Y\in \left(XIZ\right)\right)\wedge \left(A\underset{\dot{}}{-}B=X\underset{\dot{}}{-}Y\wedge B\underset{\dot{}}{-}C=Y\underset{\dot{}}{-}Z\right)\wedge \left(A\underset{\dot{}}{-}D=X\underset{\dot{}}{-}W\wedge B\underset{\dot{}}{-}D=Y\underset{\dot{}}{-}W\right)\right)\right)$$