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 ⊢ W ∈ Word V ∧ W = 3 ↔ ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V W = ⟨“ abc ”⟩

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