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