Theorem elcgrabasrd

Description: Helper theorem for the membership in the base set of the angle addition monoid. (Contributed by Thierry Arnoux, 23-Aug-2026)

	Ref	Expression
Hypotheses	elcgrabasrd.a	$$⊢A=\left\{d\in \left(P^{\left(0..^3\right)}\right)|\left(d\left(0\right)\ne d\left(1\right)\wedge d\left(1\right)\ne d\left(2\right)\right)\right\}$$
	elcgrabasrd.p	$$⊢\phi \to P\in V$$
	elcgrabasrd.x	$$⊢\phi \to X\in P$$
	elcgrabasrd.y	$$⊢\phi \to Y\in P$$
	elcgrabasrd.z	$$⊢\phi \to Z\in P$$
	elcgrabasrd.1	$$⊢\phi \to X\ne Y$$
	elcgrabasrd.2	$$⊢\phi \to Y\ne Z$$
Assertion	elcgrabasrd	$$⊢\phi \to ⟨“XYZ”⟩\in A$$

Proof

Step	Hyp	Ref	Expression
1		elcgrabasrd.a	$$⊢A=\left\{d\in \left(P^{\left(0..^3\right)}\right)|\left(d\left(0\right)\ne d\left(1\right)\wedge d\left(1\right)\ne d\left(2\right)\right)\right\}$$
2		elcgrabasrd.p	$$⊢\phi \to P\in V$$
3		elcgrabasrd.x	$$⊢\phi \to X\in P$$
4		elcgrabasrd.y	$$⊢\phi \to Y\in P$$
5		elcgrabasrd.z	$$⊢\phi \to Z\in P$$
6		elcgrabasrd.1	$$⊢\phi \to X\ne Y$$
7		elcgrabasrd.2	$$⊢\phi \to Y\ne Z$$
8		fveq1	$$⊢d=⟨“XYZ”⟩\to d\left(0\right)=⟨“XYZ”⟩\left(0\right)$$
9		fveq1	$$⊢d=⟨“XYZ”⟩\to d\left(1\right)=⟨“XYZ”⟩\left(1\right)$$
10	8 9	neeq12d	$$⊢d=⟨“XYZ”⟩\to \left(d\left(0\right)\ne d\left(1\right)\leftrightarrow ⟨“XYZ”⟩\left(0\right)\ne ⟨“XYZ”⟩\left(1\right)\right)$$
11		fveq1	$$⊢d=⟨“XYZ”⟩\to d\left(2\right)=⟨“XYZ”⟩\left(2\right)$$
12	9 11	neeq12d	$$⊢d=⟨“XYZ”⟩\to \left(d\left(1\right)\ne d\left(2\right)\leftrightarrow ⟨“XYZ”⟩\left(1\right)\ne ⟨“XYZ”⟩\left(2\right)\right)$$
13	10 12	anbi12d	$$⊢d=⟨“XYZ”⟩\to \left(\left(d\left(0\right)\ne d\left(1\right)\wedge d\left(1\right)\ne d\left(2\right)\right)\leftrightarrow \left(⟨“XYZ”⟩\left(0\right)\ne ⟨“XYZ”⟩\left(1\right)\wedge ⟨“XYZ”⟩\left(1\right)\ne ⟨“XYZ”⟩\left(2\right)\right)\right)$$
14	2 3 4 5	s3rexrd	$$⊢\phi \to ⟨“XYZ”⟩\in \left(P^{\left(0..^3\right)}\right)$$
15		s3fv0	$$⊢X\in P\to ⟨“XYZ”⟩\left(0\right)=X$$
16	3 15	syl	$$⊢\phi \to ⟨“XYZ”⟩\left(0\right)=X$$
17		s3fv1	$$⊢Y\in P\to ⟨“XYZ”⟩\left(1\right)=Y$$
18	4 17	syl	$$⊢\phi \to ⟨“XYZ”⟩\left(1\right)=Y$$
19	6 16 18	3netr4d	$$⊢\phi \to ⟨“XYZ”⟩\left(0\right)\ne ⟨“XYZ”⟩\left(1\right)$$
20		s3fv2	$$⊢Z\in P\to ⟨“XYZ”⟩\left(2\right)=Z$$
21	5 20	syl	$$⊢\phi \to ⟨“XYZ”⟩\left(2\right)=Z$$
22	7 18 21	3netr4d	$$⊢\phi \to ⟨“XYZ”⟩\left(1\right)\ne ⟨“XYZ”⟩\left(2\right)$$
23	19 22	jca	$$⊢\phi \to \left(⟨“XYZ”⟩\left(0\right)\ne ⟨“XYZ”⟩\left(1\right)\wedge ⟨“XYZ”⟩\left(1\right)\ne ⟨“XYZ”⟩\left(2\right)\right)$$
24	13 14 23	elrabd	$$⊢\phi \to ⟨“XYZ”⟩\in \left\{d\in \left(P^{\left(0..^3\right)}\right)|\left(d\left(0\right)\ne d\left(1\right)\wedge d\left(1\right)\ne d\left(2\right)\right)\right\}$$
25	24 1	eleqtrrdi	$$⊢\phi \to ⟨“XYZ”⟩\in A$$