Metamath Proof Explorer

Theorem wrdl3s3

Description: A word of length 3 is a length 3 string. (Contributed by AV, 18-May-2021)

Ref Expression
Assertion wrdl3s3 ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 3 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ )

Proof

Step Hyp Ref Expression
1 c0ex ⊢ 0 ∈ V
2 1 tpid1 ⊢ 0 ∈ { 0 , 1 , 2 }
3 fzo0to3tp ⊢ ( 0 ..^ 3 ) = { 0 , 1 , 2 }
4 2 3 eleqtrri ⊢ 0 ∈ ( 0 ..^ 3 )
5 oveq2 ⊢ ( ( ♯ ‘ 𝑊 ) = 3 → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ..^ 3 ) )
6 4 5 eleqtrrid ⊢ ( ( ♯ ‘ 𝑊 ) = 3 → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
7 wrdsymbcl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 )
8 6 7 sylan2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 3 ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 )
9 1eltp012 ⊢ 1 ∈ { 0 , 1 , 2 }
10 9 3 eleqtrri ⊢ 1 ∈ ( 0 ..^ 3 )
11 10 5 eleqtrrid ⊢ ( ( ♯ ‘ 𝑊 ) = 3 → 1 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
12 wrdsymbcl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 1 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ 1 ) ∈ 𝑉 )
13 11 12 sylan2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 3 ) → ( 𝑊 ‘ 1 ) ∈ 𝑉 )
14 2ex ⊢ 2 ∈ V
15 14 tpid3 ⊢ 2 ∈ { 0 , 1 , 2 }
16 15 3 eleqtrri ⊢ 2 ∈ ( 0 ..^ 3 )
17 16 5 eleqtrrid ⊢ ( ( ♯ ‘ 𝑊 ) = 3 → 2 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
18 wrdsymbcl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ 2 ) ∈ 𝑉 )
19 17 18 sylan2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 3 ) → ( 𝑊 ‘ 2 ) ∈ 𝑉 )
20 simpr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 3 ) → ( ♯ ‘ 𝑊 ) = 3 )
21 eqid ⊢ ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 )
22 eqid ⊢ ( 𝑊 ‘ 1 ) = ( 𝑊 ‘ 1 )
23 eqid ⊢ ( 𝑊 ‘ 2 ) = ( 𝑊 ‘ 2 )
24 21 22 23 3pm3.2i ⊢ ( ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( 𝑊 ‘ 1 ) = ( 𝑊 ‘ 1 ) ∧ ( 𝑊 ‘ 2 ) = ( 𝑊 ‘ 2 ) )
25 20 24 jctir ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 3 ) → ( ( ♯ ‘ 𝑊 ) = 3 ∧ ( ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( 𝑊 ‘ 1 ) = ( 𝑊 ‘ 1 ) ∧ ( 𝑊 ‘ 2 ) = ( 𝑊 ‘ 2 ) ) ) )
26 eqeq2 ⊢ ( 𝑎 = ( 𝑊 ‘ 0 ) → ( ( 𝑊 ‘ 0 ) = 𝑎 ↔ ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) ) )
27 26 3anbi1d ⊢ ( 𝑎 = ( 𝑊 ‘ 0 ) → ( ( ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 1 ) = 𝑏 ∧ ( 𝑊 ‘ 2 ) = 𝑐 ) ↔ ( ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( 𝑊 ‘ 1 ) = 𝑏 ∧ ( 𝑊 ‘ 2 ) = 𝑐 ) ) )
28 27 anbi2d ⊢ ( 𝑎 = ( 𝑊 ‘ 0 ) → ( ( ( ♯ ‘ 𝑊 ) = 3 ∧ ( ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 1 ) = 𝑏 ∧ ( 𝑊 ‘ 2 ) = 𝑐 ) ) ↔ ( ( ♯ ‘ 𝑊 ) = 3 ∧ ( ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( 𝑊 ‘ 1 ) = 𝑏 ∧ ( 𝑊 ‘ 2 ) = 𝑐 ) ) ) )
29 eqeq2 ⊢ ( 𝑏 = ( 𝑊 ‘ 1 ) → ( ( 𝑊 ‘ 1 ) = 𝑏 ↔ ( 𝑊 ‘ 1 ) = ( 𝑊 ‘ 1 ) ) )
30 29 3anbi2d ⊢ ( 𝑏 = ( 𝑊 ‘ 1 ) → ( ( ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( 𝑊 ‘ 1 ) = 𝑏 ∧ ( 𝑊 ‘ 2 ) = 𝑐 ) ↔ ( ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( 𝑊 ‘ 1 ) = ( 𝑊 ‘ 1 ) ∧ ( 𝑊 ‘ 2 ) = 𝑐 ) ) )
31 30 anbi2d ⊢ ( 𝑏 = ( 𝑊 ‘ 1 ) → ( ( ( ♯ ‘ 𝑊 ) = 3 ∧ ( ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( 𝑊 ‘ 1 ) = 𝑏 ∧ ( 𝑊 ‘ 2 ) = 𝑐 ) ) ↔ ( ( ♯ ‘ 𝑊 ) = 3 ∧ ( ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( 𝑊 ‘ 1 ) = ( 𝑊 ‘ 1 ) ∧ ( 𝑊 ‘ 2 ) = 𝑐 ) ) ) )
32 eqeq2 ⊢ ( 𝑐 = ( 𝑊 ‘ 2 ) → ( ( 𝑊 ‘ 2 ) = 𝑐 ↔ ( 𝑊 ‘ 2 ) = ( 𝑊 ‘ 2 ) ) )
33 32 3anbi3d ⊢ ( 𝑐 = ( 𝑊 ‘ 2 ) → ( ( ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( 𝑊 ‘ 1 ) = ( 𝑊 ‘ 1 ) ∧ ( 𝑊 ‘ 2 ) = 𝑐 ) ↔ ( ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( 𝑊 ‘ 1 ) = ( 𝑊 ‘ 1 ) ∧ ( 𝑊 ‘ 2 ) = ( 𝑊 ‘ 2 ) ) ) )
34 33 anbi2d ⊢ ( 𝑐 = ( 𝑊 ‘ 2 ) → ( ( ( ♯ ‘ 𝑊 ) = 3 ∧ ( ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( 𝑊 ‘ 1 ) = ( 𝑊 ‘ 1 ) ∧ ( 𝑊 ‘ 2 ) = 𝑐 ) ) ↔ ( ( ♯ ‘ 𝑊 ) = 3 ∧ ( ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( 𝑊 ‘ 1 ) = ( 𝑊 ‘ 1 ) ∧ ( 𝑊 ‘ 2 ) = ( 𝑊 ‘ 2 ) ) ) ) )
35 28 31 34 rspc3ev ⊢ ( ( ( ( 𝑊 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑊 ‘ 1 ) ∈ 𝑉 ∧ ( 𝑊 ‘ 2 ) ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑊 ) = 3 ∧ ( ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( 𝑊 ‘ 1 ) = ( 𝑊 ‘ 1 ) ∧ ( 𝑊 ‘ 2 ) = ( 𝑊 ‘ 2 ) ) ) ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( ♯ ‘ 𝑊 ) = 3 ∧ ( ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 1 ) = 𝑏 ∧ ( 𝑊 ‘ 2 ) = 𝑐 ) ) )
36 8 13 19 25 35 syl31anc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 3 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( ♯ ‘ 𝑊 ) = 3 ∧ ( ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 1 ) = 𝑏 ∧ ( 𝑊 ‘ 2 ) = 𝑐 ) ) )
37 df-3an ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ↔ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑐 ∈ 𝑉 ) )
38 eqwrds3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → ( 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ↔ ( ( ♯ ‘ 𝑊 ) = 3 ∧ ( ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 1 ) = 𝑏 ∧ ( 𝑊 ‘ 2 ) = 𝑐 ) ) ) )
39 38 ex ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ↔ ( ( ♯ ‘ 𝑊 ) = 3 ∧ ( ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 1 ) = 𝑏 ∧ ( 𝑊 ‘ 2 ) = 𝑐 ) ) ) ) )
40 37 39 biimtrrid ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑐 ∈ 𝑉 ) → ( 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ↔ ( ( ♯ ‘ 𝑊 ) = 3 ∧ ( ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 1 ) = 𝑏 ∧ ( 𝑊 ‘ 2 ) = 𝑐 ) ) ) ) )
41 40 expd ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑐 ∈ 𝑉 → ( 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ↔ ( ( ♯ ‘ 𝑊 ) = 3 ∧ ( ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 1 ) = 𝑏 ∧ ( 𝑊 ‘ 2 ) = 𝑐 ) ) ) ) ) )
42 41 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 3 ) → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑐 ∈ 𝑉 → ( 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ↔ ( ( ♯ ‘ 𝑊 ) = 3 ∧ ( ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 1 ) = 𝑏 ∧ ( 𝑊 ‘ 2 ) = 𝑐 ) ) ) ) ) )
43 42 imp31 ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 3 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) → ( 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ↔ ( ( ♯ ‘ 𝑊 ) = 3 ∧ ( ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 1 ) = 𝑏 ∧ ( 𝑊 ‘ 2 ) = 𝑐 ) ) ) )
44 43 rexbidva ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 3 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ∃ 𝑐 ∈ 𝑉 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ↔ ∃ 𝑐 ∈ 𝑉 ( ( ♯ ‘ 𝑊 ) = 3 ∧ ( ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 1 ) = 𝑏 ∧ ( 𝑊 ‘ 2 ) = 𝑐 ) ) ) )
45 44 2rexbidva ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 3 ) → ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( ♯ ‘ 𝑊 ) = 3 ∧ ( ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 1 ) = 𝑏 ∧ ( 𝑊 ‘ 2 ) = 𝑐 ) ) ) )
46 36 45 mpbird ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 3 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ )
47 s3cl ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ⟨“ 𝑎 𝑏 𝑐 ”⟩ ∈ Word 𝑉 )
48 47 ad4ant123 ⊢ ( ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑐 ∈ 𝑉 ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) → ⟨“ 𝑎 𝑏 𝑐 ”⟩ ∈ Word 𝑉 )
49 s3len ⊢ ( ♯ ‘ ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) = 3
50 48 49 jctir ⊢ ( ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑐 ∈ 𝑉 ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) → ( ⟨“ 𝑎 𝑏 𝑐 ”⟩ ∈ Word 𝑉 ∧ ( ♯ ‘ ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) = 3 ) )
51 eleq1 ⊢ ( 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ → ( 𝑊 ∈ Word 𝑉 ↔ ⟨“ 𝑎 𝑏 𝑐 ”⟩ ∈ Word 𝑉 ) )
52 fveqeq2 ⊢ ( 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ → ( ( ♯ ‘ 𝑊 ) = 3 ↔ ( ♯ ‘ ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) = 3 ) )
53 51 52 anbi12d ⊢ ( 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 3 ) ↔ ( ⟨“ 𝑎 𝑏 𝑐 ”⟩ ∈ Word 𝑉 ∧ ( ♯ ‘ ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) = 3 ) ) )
54 53 adantl ⊢ ( ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑐 ∈ 𝑉 ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 3 ) ↔ ( ⟨“ 𝑎 𝑏 𝑐 ”⟩ ∈ Word 𝑉 ∧ ( ♯ ‘ ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) = 3 ) ) )
55 50 54 mpbird ⊢ ( ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑐 ∈ 𝑉 ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 3 ) )
56 55 rexlimdva2 ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( ∃ 𝑐 ∈ 𝑉 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 3 ) ) )
57 56 rexlimivv ⊢ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 3 ) )
58 46 57 impbii ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 3 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ )