Metamath Proof Explorer

Theorem elcgrabasi

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 elcgrabasi.1 ⊢ P ∈ V
elcgrabasi.2 ⊢ A = d ∈ P 0 ..^ 3 | d ⁡ 0 ≠ d ⁡ 1 ∧ d ⁡ 1 ≠ d ⁡ 2
elcgrabasi.3 ⊢ φ → E ∈ A
Assertion elcgrabasi ⊢ φ → ∃ x ∈ P ∃ y ∈ P ∃ z ∈ P E = ⟨“ xyz ”⟩ ∧ x ≠ y ∧ y ≠ z

Proof

Step Hyp Ref Expression
1 elcgrabasi.1 ⊢ P ∈ V
2 elcgrabasi.2 ⊢ A = d ∈ P 0 ..^ 3 | d ⁡ 0 ≠ d ⁡ 1 ∧ d ⁡ 1 ≠ d ⁡ 2
3 elcgrabasi.3 ⊢ φ → E ∈ A
4 id ⊢ x = E ⁡ 0 → x = E ⁡ 0
5 eqidd ⊢ x = E ⁡ 0 → y = y
6 eqidd ⊢ x = E ⁡ 0 → z = z
7 4 5 6 s3eqd ⊢ x = E ⁡ 0 → ⟨“ xyz ”⟩ = ⟨“ E ⁡ 0 yz ”⟩
8 7 eqeq2d ⊢ x = E ⁡ 0 → E = ⟨“ xyz ”⟩ ↔ E = ⟨“ E ⁡ 0 yz ”⟩
9 4 neeq1d ⊢ x = E ⁡ 0 → x ≠ y ↔ E ⁡ 0 ≠ y
10 9 anbi1d ⊢ x = E ⁡ 0 → x ≠ y ∧ y ≠ z ↔ E ⁡ 0 ≠ y ∧ y ≠ z
11 8 10 anbi12d ⊢ x = E ⁡ 0 → E = ⟨“ xyz ”⟩ ∧ x ≠ y ∧ y ≠ z ↔ E = ⟨“ E ⁡ 0 yz ”⟩ ∧ E ⁡ 0 ≠ y ∧ y ≠ z
12 s3eq2 ⊢ y = E ⁡ 1 → ⟨“ E ⁡ 0 yz ”⟩ = ⟨“ E ⁡ 0 E ⁡ 1 z ”⟩
13 12 eqeq2d ⊢ y = E ⁡ 1 → E = ⟨“ E ⁡ 0 yz ”⟩ ↔ E = ⟨“ E ⁡ 0 E ⁡ 1 z ”⟩
14 neeq2 ⊢ y = E ⁡ 1 → E ⁡ 0 ≠ y ↔ E ⁡ 0 ≠ E ⁡ 1
15 neeq1 ⊢ y = E ⁡ 1 → y ≠ z ↔ E ⁡ 1 ≠ z
16 14 15 anbi12d ⊢ y = E ⁡ 1 → E ⁡ 0 ≠ y ∧ y ≠ z ↔ E ⁡ 0 ≠ E ⁡ 1 ∧ E ⁡ 1 ≠ z
17 13 16 anbi12d ⊢ y = E ⁡ 1 → E = ⟨“ E ⁡ 0 yz ”⟩ ∧ E ⁡ 0 ≠ y ∧ y ≠ z ↔ E = ⟨“ E ⁡ 0 E ⁡ 1 z ”⟩ ∧ E ⁡ 0 ≠ E ⁡ 1 ∧ E ⁡ 1 ≠ z
18 eqidd ⊢ z = E ⁡ 2 → E ⁡ 0 = E ⁡ 0
19 eqidd ⊢ z = E ⁡ 2 → E ⁡ 1 = E ⁡ 1
20 id ⊢ z = E ⁡ 2 → z = E ⁡ 2
21 18 19 20 s3eqd ⊢ z = E ⁡ 2 → ⟨“ E ⁡ 0 E ⁡ 1 z ”⟩ = ⟨“ E ⁡ 0 E ⁡ 1 E ⁡ 2 ”⟩
22 21 eqeq2d ⊢ z = E ⁡ 2 → E = ⟨“ E ⁡ 0 E ⁡ 1 z ”⟩ ↔ E = ⟨“ E ⁡ 0 E ⁡ 1 E ⁡ 2 ”⟩
23 biidd ⊢ z = E ⁡ 2 → E ⁡ 0 ≠ E ⁡ 1 ↔ E ⁡ 0 ≠ E ⁡ 1
24 20 neeq2d ⊢ z = E ⁡ 2 → E ⁡ 1 ≠ z ↔ E ⁡ 1 ≠ E ⁡ 2
25 23 24 anbi12d ⊢ z = E ⁡ 2 → E ⁡ 0 ≠ E ⁡ 1 ∧ E ⁡ 1 ≠ z ↔ E ⁡ 0 ≠ E ⁡ 1 ∧ E ⁡ 1 ≠ E ⁡ 2
26 22 25 anbi12d ⊢ z = E ⁡ 2 → E = ⟨“ E ⁡ 0 E ⁡ 1 z ”⟩ ∧ E ⁡ 0 ≠ E ⁡ 1 ∧ E ⁡ 1 ≠ z ↔ E = ⟨“ E ⁡ 0 E ⁡ 1 E ⁡ 2 ”⟩ ∧ E ⁡ 0 ≠ E ⁡ 1 ∧ E ⁡ 1 ≠ E ⁡ 2
27 fzo0to3tp ⊢ 0 ..^ 3 = 0 1 2
28 27 a1i ⊢ φ → 0 ..^ 3 = 0 1 2
29 2 ssrab3 ⊢ A ⊆ P 0 ..^ 3
30 29 3 sselid ⊢ φ → E ∈ P 0 ..^ 3
31 30 elmaprd ⊢ φ → E : 0 ..^ 3 ⟶ P
32 28 31 feq2dd ⊢ φ → E : 0 1 2 ⟶ P
33 c0ex ⊢ 0 ∈ V
34 33 tpid1 ⊢ 0 ∈ 0 1 2
35 34 a1i ⊢ φ → 0 ∈ 0 1 2
36 32 35 ffvelcdmd ⊢ φ → E ⁡ 0 ∈ P
37 1eltp012 ⊢ 1 ∈ 0 1 2
38 37 a1i ⊢ φ → 1 ∈ 0 1 2
39 32 38 ffvelcdmd ⊢ φ → E ⁡ 1 ∈ P
40 2ex ⊢ 2 ∈ V
41 40 tpid3 ⊢ 2 ∈ 0 1 2
42 41 a1i ⊢ φ → 2 ∈ 0 1 2
43 32 42 ffvelcdmd ⊢ φ → E ⁡ 2 ∈ P
44 iswrdi ⊢ E : 0 ..^ 3 ⟶ P → E ∈ Word P
45 31 44 syl ⊢ φ → E ∈ Word P
46 31 ffnd ⊢ φ → E Fn 0 ..^ 3
47 hashfn ⊢ E Fn 0 ..^ 3 → E = 0 ..^ 3
48 46 47 syl ⊢ φ → E = 0 ..^ 3
49 3nn0 ⊢ 3 ∈ ℕ 0
50 hashfzo0 ⊢ 3 ∈ ℕ 0 → 0 ..^ 3 = 3
51 49 50 ax-mp ⊢ 0 ..^ 3 = 3
52 48 51 eqtrdi ⊢ φ → E = 3
53 wrdlen3s3 ⊢ E ∈ Word P ∧ E = 3 → E = ⟨“ E ⁡ 0 E ⁡ 1 E ⁡ 2 ”⟩
54 45 52 53 syl2anc ⊢ φ → E = ⟨“ E ⁡ 0 E ⁡ 1 E ⁡ 2 ”⟩
55 fveq1 ⊢ d = E → d ⁡ 0 = E ⁡ 0
56 fveq1 ⊢ d = E → d ⁡ 1 = E ⁡ 1
57 55 56 neeq12d ⊢ d = E → d ⁡ 0 ≠ d ⁡ 1 ↔ E ⁡ 0 ≠ E ⁡ 1
58 fveq1 ⊢ d = E → d ⁡ 2 = E ⁡ 2
59 56 58 neeq12d ⊢ d = E → d ⁡ 1 ≠ d ⁡ 2 ↔ E ⁡ 1 ≠ E ⁡ 2
60 57 59 anbi12d ⊢ d = E → d ⁡ 0 ≠ d ⁡ 1 ∧ d ⁡ 1 ≠ d ⁡ 2 ↔ E ⁡ 0 ≠ E ⁡ 1 ∧ E ⁡ 1 ≠ E ⁡ 2
61 2 eleq2i ⊢ E ∈ A ↔ E ∈ d ∈ P 0 ..^ 3 | d ⁡ 0 ≠ d ⁡ 1 ∧ d ⁡ 1 ≠ d ⁡ 2
62 3 61 sylib ⊢ φ → E ∈ d ∈ P 0 ..^ 3 | d ⁡ 0 ≠ d ⁡ 1 ∧ d ⁡ 1 ≠ d ⁡ 2
63 60 62 elrabrd ⊢ φ → E ⁡ 0 ≠ E ⁡ 1 ∧ E ⁡ 1 ≠ E ⁡ 2
64 54 63 jca ⊢ φ → E = ⟨“ E ⁡ 0 E ⁡ 1 E ⁡ 2 ”⟩ ∧ E ⁡ 0 ≠ E ⁡ 1 ∧ E ⁡ 1 ≠ E ⁡ 2
65 11 17 26 36 39 43 64 3rspcedvdw ⊢ φ → ∃ x ∈ P ∃ y ∈ P ∃ z ∈ P E = ⟨“ xyz ”⟩ ∧ x ≠ y ∧ y ≠ z