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