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 ⊢ 𝑃 ∈ V
elcgrabasi.2 ⊢ 𝐴 = { 𝑑 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) }
elcgrabasi.3 ⊢ ( 𝜑 → 𝐸 ∈ 𝐴 )
Assertion elcgrabasi ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 elcgrabasi.1 ⊢ 𝑃 ∈ V
2 elcgrabasi.2 ⊢ 𝐴 = { 𝑑 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) }
3 elcgrabasi.3 ⊢ ( 𝜑 → 𝐸 ∈ 𝐴 )
4 id ⊢ ( 𝑥 = ( 𝐸 ‘ 0 ) → 𝑥 = ( 𝐸 ‘ 0 ) )
5 eqidd ⊢ ( 𝑥 = ( 𝐸 ‘ 0 ) → 𝑦 = 𝑦 )
6 eqidd ⊢ ( 𝑥 = ( 𝐸 ‘ 0 ) → 𝑧 = 𝑧 )
7 4 5 6 s3eqd ⊢ ( 𝑥 = ( 𝐸 ‘ 0 ) → ⟨“ 𝑥 𝑦 𝑧 ”⟩ = ⟨“ ( 𝐸 ‘ 0 ) 𝑦 𝑧 ”⟩ )
8 7 eqeq2d ⊢ ( 𝑥 = ( 𝐸 ‘ 0 ) → ( 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ↔ 𝐸 = ⟨“ ( 𝐸 ‘ 0 ) 𝑦 𝑧 ”⟩ ) )
9 4 neeq1d ⊢ ( 𝑥 = ( 𝐸 ‘ 0 ) → ( 𝑥 ≠ 𝑦 ↔ ( 𝐸 ‘ 0 ) ≠ 𝑦 ) )
10 9 anbi1d ⊢ ( 𝑥 = ( 𝐸 ‘ 0 ) → ( ( 𝑥 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ) ↔ ( ( 𝐸 ‘ 0 ) ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ) ) )
11 8 10 anbi12d ⊢ ( 𝑥 = ( 𝐸 ‘ 0 ) → ( ( 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ) ) ↔ ( 𝐸 = ⟨“ ( 𝐸 ‘ 0 ) 𝑦 𝑧 ”⟩ ∧ ( ( 𝐸 ‘ 0 ) ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ) ) ) )
12 s3eq2 ⊢ ( 𝑦 = ( 𝐸 ‘ 1 ) → ⟨“ ( 𝐸 ‘ 0 ) 𝑦 𝑧 ”⟩ = ⟨“ ( 𝐸 ‘ 0 ) ( 𝐸 ‘ 1 ) 𝑧 ”⟩ )
13 12 eqeq2d ⊢ ( 𝑦 = ( 𝐸 ‘ 1 ) → ( 𝐸 = ⟨“ ( 𝐸 ‘ 0 ) 𝑦 𝑧 ”⟩ ↔ 𝐸 = ⟨“ ( 𝐸 ‘ 0 ) ( 𝐸 ‘ 1 ) 𝑧 ”⟩ ) )
14 neeq2 ⊢ ( 𝑦 = ( 𝐸 ‘ 1 ) → ( ( 𝐸 ‘ 0 ) ≠ 𝑦 ↔ ( 𝐸 ‘ 0 ) ≠ ( 𝐸 ‘ 1 ) ) )
15 neeq1 ⊢ ( 𝑦 = ( 𝐸 ‘ 1 ) → ( 𝑦 ≠ 𝑧 ↔ ( 𝐸 ‘ 1 ) ≠ 𝑧 ) )
16 14 15 anbi12d ⊢ ( 𝑦 = ( 𝐸 ‘ 1 ) → ( ( ( 𝐸 ‘ 0 ) ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ) ↔ ( ( 𝐸 ‘ 0 ) ≠ ( 𝐸 ‘ 1 ) ∧ ( 𝐸 ‘ 1 ) ≠ 𝑧 ) ) )
17 13 16 anbi12d ⊢ ( 𝑦 = ( 𝐸 ‘ 1 ) → ( ( 𝐸 = ⟨“ ( 𝐸 ‘ 0 ) 𝑦 𝑧 ”⟩ ∧ ( ( 𝐸 ‘ 0 ) ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ) ) ↔ ( 𝐸 = ⟨“ ( 𝐸 ‘ 0 ) ( 𝐸 ‘ 1 ) 𝑧 ”⟩ ∧ ( ( 𝐸 ‘ 0 ) ≠ ( 𝐸 ‘ 1 ) ∧ ( 𝐸 ‘ 1 ) ≠ 𝑧 ) ) ) )
18 eqidd ⊢ ( 𝑧 = ( 𝐸 ‘ 2 ) → ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ 0 ) )
19 eqidd ⊢ ( 𝑧 = ( 𝐸 ‘ 2 ) → ( 𝐸 ‘ 1 ) = ( 𝐸 ‘ 1 ) )
20 id ⊢ ( 𝑧 = ( 𝐸 ‘ 2 ) → 𝑧 = ( 𝐸 ‘ 2 ) )
21 18 19 20 s3eqd ⊢ ( 𝑧 = ( 𝐸 ‘ 2 ) → ⟨“ ( 𝐸 ‘ 0 ) ( 𝐸 ‘ 1 ) 𝑧 ”⟩ = ⟨“ ( 𝐸 ‘ 0 ) ( 𝐸 ‘ 1 ) ( 𝐸 ‘ 2 ) ”⟩ )
22 21 eqeq2d ⊢ ( 𝑧 = ( 𝐸 ‘ 2 ) → ( 𝐸 = ⟨“ ( 𝐸 ‘ 0 ) ( 𝐸 ‘ 1 ) 𝑧 ”⟩ ↔ 𝐸 = ⟨“ ( 𝐸 ‘ 0 ) ( 𝐸 ‘ 1 ) ( 𝐸 ‘ 2 ) ”⟩ ) )
23 biidd ⊢ ( 𝑧 = ( 𝐸 ‘ 2 ) → ( ( 𝐸 ‘ 0 ) ≠ ( 𝐸 ‘ 1 ) ↔ ( 𝐸 ‘ 0 ) ≠ ( 𝐸 ‘ 1 ) ) )
24 20 neeq2d ⊢ ( 𝑧 = ( 𝐸 ‘ 2 ) → ( ( 𝐸 ‘ 1 ) ≠ 𝑧 ↔ ( 𝐸 ‘ 1 ) ≠ ( 𝐸 ‘ 2 ) ) )
25 23 24 anbi12d ⊢ ( 𝑧 = ( 𝐸 ‘ 2 ) → ( ( ( 𝐸 ‘ 0 ) ≠ ( 𝐸 ‘ 1 ) ∧ ( 𝐸 ‘ 1 ) ≠ 𝑧 ) ↔ ( ( 𝐸 ‘ 0 ) ≠ ( 𝐸 ‘ 1 ) ∧ ( 𝐸 ‘ 1 ) ≠ ( 𝐸 ‘ 2 ) ) ) )
26 22 25 anbi12d ⊢ ( 𝑧 = ( 𝐸 ‘ 2 ) → ( ( 𝐸 = ⟨“ ( 𝐸 ‘ 0 ) ( 𝐸 ‘ 1 ) 𝑧 ”⟩ ∧ ( ( 𝐸 ‘ 0 ) ≠ ( 𝐸 ‘ 1 ) ∧ ( 𝐸 ‘ 1 ) ≠ 𝑧 ) ) ↔ ( 𝐸 = ⟨“ ( 𝐸 ‘ 0 ) ( 𝐸 ‘ 1 ) ( 𝐸 ‘ 2 ) ”⟩ ∧ ( ( 𝐸 ‘ 0 ) ≠ ( 𝐸 ‘ 1 ) ∧ ( 𝐸 ‘ 1 ) ≠ ( 𝐸 ‘ 2 ) ) ) ) )
27 fzo0to3tp ⊢ ( 0 ..^ 3 ) = { 0 , 1 , 2 }
28 27 a1i ⊢ ( 𝜑 → ( 0 ..^ 3 ) = { 0 , 1 , 2 } )
29 2 ssrab3 ⊢ 𝐴 ⊆ ( 𝑃 ↑m ( 0 ..^ 3 ) )
30 29 3 sselid ⊢ ( 𝜑 → 𝐸 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
31 30 elmaprd ⊢ ( 𝜑 → 𝐸 : ( 0 ..^ 3 ) ⟶ 𝑃 )
32 28 31 feq2dd ⊢ ( 𝜑 → 𝐸 : { 0 , 1 , 2 } ⟶ 𝑃 )
33 c0ex ⊢ 0 ∈ V
34 33 tpid1 ⊢ 0 ∈ { 0 , 1 , 2 }
35 34 a1i ⊢ ( 𝜑 → 0 ∈ { 0 , 1 , 2 } )
36 32 35 ffvelcdmd ⊢ ( 𝜑 → ( 𝐸 ‘ 0 ) ∈ 𝑃 )
37 1eltp012 ⊢ 1 ∈ { 0 , 1 , 2 }
38 37 a1i ⊢ ( 𝜑 → 1 ∈ { 0 , 1 , 2 } )
39 32 38 ffvelcdmd ⊢ ( 𝜑 → ( 𝐸 ‘ 1 ) ∈ 𝑃 )
40 2ex ⊢ 2 ∈ V
41 40 tpid3 ⊢ 2 ∈ { 0 , 1 , 2 }
42 41 a1i ⊢ ( 𝜑 → 2 ∈ { 0 , 1 , 2 } )
43 32 42 ffvelcdmd ⊢ ( 𝜑 → ( 𝐸 ‘ 2 ) ∈ 𝑃 )
44 iswrdi ⊢ ( 𝐸 : ( 0 ..^ 3 ) ⟶ 𝑃 → 𝐸 ∈ Word 𝑃 )
45 31 44 syl ⊢ ( 𝜑 → 𝐸 ∈ Word 𝑃 )
46 31 ffnd ⊢ ( 𝜑 → 𝐸 Fn ( 0 ..^ 3 ) )
47 hashfn ⊢ ( 𝐸 Fn ( 0 ..^ 3 ) → ( ♯ ‘ 𝐸 ) = ( ♯ ‘ ( 0 ..^ 3 ) ) )
48 46 47 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐸 ) = ( ♯ ‘ ( 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 ⊢ ( 𝜑 → ( ♯ ‘ 𝐸 ) = 3 )
53 wrdlen3s3 ⊢ ( ( 𝐸 ∈ Word 𝑃 ∧ ( ♯ ‘ 𝐸 ) = 3 ) → 𝐸 = ⟨“ ( 𝐸 ‘ 0 ) ( 𝐸 ‘ 1 ) ( 𝐸 ‘ 2 ) ”⟩ )
54 45 52 53 syl2anc ⊢ ( 𝜑 → 𝐸 = ⟨“ ( 𝐸 ‘ 0 ) ( 𝐸 ‘ 1 ) ( 𝐸 ‘ 2 ) ”⟩ )
55 fveq1 ⊢ ( 𝑑 = 𝐸 → ( 𝑑 ‘ 0 ) = ( 𝐸 ‘ 0 ) )
56 fveq1 ⊢ ( 𝑑 = 𝐸 → ( 𝑑 ‘ 1 ) = ( 𝐸 ‘ 1 ) )
57 55 56 neeq12d ⊢ ( 𝑑 = 𝐸 → ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ↔ ( 𝐸 ‘ 0 ) ≠ ( 𝐸 ‘ 1 ) ) )
58 fveq1 ⊢ ( 𝑑 = 𝐸 → ( 𝑑 ‘ 2 ) = ( 𝐸 ‘ 2 ) )
59 56 58 neeq12d ⊢ ( 𝑑 = 𝐸 → ( ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ↔ ( 𝐸 ‘ 1 ) ≠ ( 𝐸 ‘ 2 ) ) )
60 57 59 anbi12d ⊢ ( 𝑑 = 𝐸 → ( ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) ↔ ( ( 𝐸 ‘ 0 ) ≠ ( 𝐸 ‘ 1 ) ∧ ( 𝐸 ‘ 1 ) ≠ ( 𝐸 ‘ 2 ) ) ) )
61 2 eleq2i ⊢ ( 𝐸 ∈ 𝐴 ↔ 𝐸 ∈ { 𝑑 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) } )
62 3 61 sylib ⊢ ( 𝜑 → 𝐸 ∈ { 𝑑 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) } )
63 60 62 elrabrd ⊢ ( 𝜑 → ( ( 𝐸 ‘ 0 ) ≠ ( 𝐸 ‘ 1 ) ∧ ( 𝐸 ‘ 1 ) ≠ ( 𝐸 ‘ 2 ) ) )
64 54 63 jca ⊢ ( 𝜑 → ( 𝐸 = ⟨“ ( 𝐸 ‘ 0 ) ( 𝐸 ‘ 1 ) ( 𝐸 ‘ 2 ) ”⟩ ∧ ( ( 𝐸 ‘ 0 ) ≠ ( 𝐸 ‘ 1 ) ∧ ( 𝐸 ‘ 1 ) ≠ ( 𝐸 ‘ 2 ) ) ) )
65 11 17 26 36 39 43 64 3rspcedvdw ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ) ) )