Metamath Proof Explorer

Theorem s3rex

Description: Membership in a family of words of length 3. (Contributed by Thierry Arnoux, 23-Aug-2026)

Ref Expression
Hypothesis s3rex.1 ⊢ 𝑆 ∈ V
Assertion s3rex ( 𝐴 ∈ ( 𝑆 ↑m ( 0 ..^ 3 ) ) ↔ ∃ 𝑥 ∈ 𝑆 ∃ 𝑦 ∈ 𝑆 ∃ 𝑧 ∈ 𝑆 𝐴 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ )

Proof

Step Hyp Ref Expression
1 s3rex.1 ⊢ 𝑆 ∈ V
2 id ⊢ ( 𝑥 = ( 𝐴 ‘ 0 ) → 𝑥 = ( 𝐴 ‘ 0 ) )
3 eqidd ⊢ ( 𝑥 = ( 𝐴 ‘ 0 ) → 𝑦 = 𝑦 )
4 eqidd ⊢ ( 𝑥 = ( 𝐴 ‘ 0 ) → 𝑧 = 𝑧 )
5 2 3 4 s3eqd ⊢ ( 𝑥 = ( 𝐴 ‘ 0 ) → ⟨“ 𝑥 𝑦 𝑧 ”⟩ = ⟨“ ( 𝐴 ‘ 0 ) 𝑦 𝑧 ”⟩ )
6 5 eqeq2d ⊢ ( 𝑥 = ( 𝐴 ‘ 0 ) → ( 𝐴 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ↔ 𝐴 = ⟨“ ( 𝐴 ‘ 0 ) 𝑦 𝑧 ”⟩ ) )
7 s3eq2 ⊢ ( 𝑦 = ( 𝐴 ‘ 1 ) → ⟨“ ( 𝐴 ‘ 0 ) 𝑦 𝑧 ”⟩ = ⟨“ ( 𝐴 ‘ 0 ) ( 𝐴 ‘ 1 ) 𝑧 ”⟩ )
8 7 eqeq2d ⊢ ( 𝑦 = ( 𝐴 ‘ 1 ) → ( 𝐴 = ⟨“ ( 𝐴 ‘ 0 ) 𝑦 𝑧 ”⟩ ↔ 𝐴 = ⟨“ ( 𝐴 ‘ 0 ) ( 𝐴 ‘ 1 ) 𝑧 ”⟩ ) )
9 eqidd ⊢ ( 𝑧 = ( 𝐴 ‘ 2 ) → ( 𝐴 ‘ 0 ) = ( 𝐴 ‘ 0 ) )
10 eqidd ⊢ ( 𝑧 = ( 𝐴 ‘ 2 ) → ( 𝐴 ‘ 1 ) = ( 𝐴 ‘ 1 ) )
11 id ⊢ ( 𝑧 = ( 𝐴 ‘ 2 ) → 𝑧 = ( 𝐴 ‘ 2 ) )
12 9 10 11 s3eqd ⊢ ( 𝑧 = ( 𝐴 ‘ 2 ) → ⟨“ ( 𝐴 ‘ 0 ) ( 𝐴 ‘ 1 ) 𝑧 ”⟩ = ⟨“ ( 𝐴 ‘ 0 ) ( 𝐴 ‘ 1 ) ( 𝐴 ‘ 2 ) ”⟩ )
13 12 eqeq2d ⊢ ( 𝑧 = ( 𝐴 ‘ 2 ) → ( 𝐴 = ⟨“ ( 𝐴 ‘ 0 ) ( 𝐴 ‘ 1 ) 𝑧 ”⟩ ↔ 𝐴 = ⟨“ ( 𝐴 ‘ 0 ) ( 𝐴 ‘ 1 ) ( 𝐴 ‘ 2 ) ”⟩ ) )
14 elmapi ⊢ ( 𝐴 ∈ ( 𝑆 ↑m ( 0 ..^ 3 ) ) → 𝐴 : ( 0 ..^ 3 ) ⟶ 𝑆 )
15 c0ex ⊢ 0 ∈ V
16 15 tpid1 ⊢ 0 ∈ { 0 , 1 , 2 }
17 fzo0to3tp ⊢ ( 0 ..^ 3 ) = { 0 , 1 , 2 }
18 16 17 eleqtrri ⊢ 0 ∈ ( 0 ..^ 3 )
19 18 a1i ⊢ ( 𝐴 ∈ ( 𝑆 ↑m ( 0 ..^ 3 ) ) → 0 ∈ ( 0 ..^ 3 ) )
20 14 19 ffvelcdmd ⊢ ( 𝐴 ∈ ( 𝑆 ↑m ( 0 ..^ 3 ) ) → ( 𝐴 ‘ 0 ) ∈ 𝑆 )
21 1eltp012 ⊢ 1 ∈ { 0 , 1 , 2 }
22 21 17 eleqtrri ⊢ 1 ∈ ( 0 ..^ 3 )
23 22 a1i ⊢ ( 𝐴 ∈ ( 𝑆 ↑m ( 0 ..^ 3 ) ) → 1 ∈ ( 0 ..^ 3 ) )
24 14 23 ffvelcdmd ⊢ ( 𝐴 ∈ ( 𝑆 ↑m ( 0 ..^ 3 ) ) → ( 𝐴 ‘ 1 ) ∈ 𝑆 )
25 2ex ⊢ 2 ∈ V
26 25 tpid3 ⊢ 2 ∈ { 0 , 1 , 2 }
27 26 17 eleqtrri ⊢ 2 ∈ ( 0 ..^ 3 )
28 27 a1i ⊢ ( 𝐴 ∈ ( 𝑆 ↑m ( 0 ..^ 3 ) ) → 2 ∈ ( 0 ..^ 3 ) )
29 14 28 ffvelcdmd ⊢ ( 𝐴 ∈ ( 𝑆 ↑m ( 0 ..^ 3 ) ) → ( 𝐴 ‘ 2 ) ∈ 𝑆 )
30 iswrdi ⊢ ( 𝐴 : ( 0 ..^ 3 ) ⟶ 𝑆 → 𝐴 ∈ Word 𝑆 )
31 14 30 syl ⊢ ( 𝐴 ∈ ( 𝑆 ↑m ( 0 ..^ 3 ) ) → 𝐴 ∈ Word 𝑆 )
32 elmapfn ⊢ ( 𝐴 ∈ ( 𝑆 ↑m ( 0 ..^ 3 ) ) → 𝐴 Fn ( 0 ..^ 3 ) )
33 hashfn ⊢ ( 𝐴 Fn ( 0 ..^ 3 ) → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ ( 0 ..^ 3 ) ) )
34 32 33 syl ⊢ ( 𝐴 ∈ ( 𝑆 ↑m ( 0 ..^ 3 ) ) → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ ( 0 ..^ 3 ) ) )
35 3nn0 ⊢ 3 ∈ ℕ0
36 hashfzo0 ⊢ ( 3 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 3 ) ) = 3 )
37 35 36 ax-mp ⊢ ( ♯ ‘ ( 0 ..^ 3 ) ) = 3
38 34 37 eqtrdi ⊢ ( 𝐴 ∈ ( 𝑆 ↑m ( 0 ..^ 3 ) ) → ( ♯ ‘ 𝐴 ) = 3 )
39 wrdlen3s3 ⊢ ( ( 𝐴 ∈ Word 𝑆 ∧ ( ♯ ‘ 𝐴 ) = 3 ) → 𝐴 = ⟨“ ( 𝐴 ‘ 0 ) ( 𝐴 ‘ 1 ) ( 𝐴 ‘ 2 ) ”⟩ )
40 31 38 39 syl2anc ⊢ ( 𝐴 ∈ ( 𝑆 ↑m ( 0 ..^ 3 ) ) → 𝐴 = ⟨“ ( 𝐴 ‘ 0 ) ( 𝐴 ‘ 1 ) ( 𝐴 ‘ 2 ) ”⟩ )
41 6 8 13 20 24 29 40 3rspcedvdw ⊢ ( 𝐴 ∈ ( 𝑆 ↑m ( 0 ..^ 3 ) ) → ∃ 𝑥 ∈ 𝑆 ∃ 𝑦 ∈ 𝑆 ∃ 𝑧 ∈ 𝑆 𝐴 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ )
42 1 a1i ⊢ ( ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝐴 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) → 𝑆 ∈ V )
43 ovexd ⊢ ( ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝐴 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) → ( 0 ..^ 3 ) ∈ V )
44 simpr ⊢ ( ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝐴 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) → 𝐴 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ )
45 44 fveq2d ⊢ ( ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝐴 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) )
46 s3len ⊢ ( ♯ ‘ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) = 3
47 45 46 eqtr2di ⊢ ( ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝐴 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) → 3 = ( ♯ ‘ 𝐴 ) )
48 simplll ⊢ ( ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝐴 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) → 𝑥 ∈ 𝑆 )
49 simpllr ⊢ ( ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝐴 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) → 𝑦 ∈ 𝑆 )
50 simplr ⊢ ( ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝐴 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) → 𝑧 ∈ 𝑆 )
51 48 49 50 s3cld ⊢ ( ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝐴 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) → ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∈ Word 𝑆 )
52 44 51 eqeltrd ⊢ ( ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝐴 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) → 𝐴 ∈ Word 𝑆 )
53 47 52 wrdfd ⊢ ( ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝐴 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) → 𝐴 : ( 0 ..^ 3 ) ⟶ 𝑆 )
54 42 43 53 elmapdd ⊢ ( ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝐴 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) → 𝐴 ∈ ( 𝑆 ↑m ( 0 ..^ 3 ) ) )
55 54 rexlimdva2 ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( ∃ 𝑧 ∈ 𝑆 𝐴 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ → 𝐴 ∈ ( 𝑆 ↑m ( 0 ..^ 3 ) ) ) )
56 55 rexlimivv ⊢ ( ∃ 𝑥 ∈ 𝑆 ∃ 𝑦 ∈ 𝑆 ∃ 𝑧 ∈ 𝑆 𝐴 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ → 𝐴 ∈ ( 𝑆 ↑m ( 0 ..^ 3 ) ) )
57 41 56 impbii ⊢ ( 𝐴 ∈ ( 𝑆 ↑m ( 0 ..^ 3 ) ) ↔ ∃ 𝑥 ∈ 𝑆 ∃ 𝑦 ∈ 𝑆 ∃ 𝑧 ∈ 𝑆 𝐴 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ )