Step | Hyp | Ref
| Expression |
1 | | c0ex 11208 |
. . . . . . . 8
⊢ 0 ∈
V |
2 | 1 | tpid1 4773 |
. . . . . . 7
⊢ 0 ∈
{0, 1, 2} |
3 | | fzo0to3tp 13718 |
. . . . . . 7
⊢ (0..^3) =
{0, 1, 2} |
4 | 2, 3 | eleqtrri 2833 |
. . . . . 6
⊢ 0 ∈
(0..^3) |
5 | | oveq2 7417 |
. . . . . 6
⊢
((♯‘𝑊) =
3 → (0..^(♯‘𝑊)) = (0..^3)) |
6 | 4, 5 | eleqtrrid 2841 |
. . . . 5
⊢
((♯‘𝑊) =
3 → 0 ∈ (0..^(♯‘𝑊))) |
7 | | wrdsymbcl 14477 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 0 ∈ (0..^(♯‘𝑊))) → (𝑊‘0) ∈ 𝑉) |
8 | 6, 7 | sylan2 594 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) → (𝑊‘0) ∈ 𝑉) |
9 | | 1ex 11210 |
. . . . . . . 8
⊢ 1 ∈
V |
10 | 9 | tpid2 4775 |
. . . . . . 7
⊢ 1 ∈
{0, 1, 2} |
11 | 10, 3 | eleqtrri 2833 |
. . . . . 6
⊢ 1 ∈
(0..^3) |
12 | 11, 5 | eleqtrrid 2841 |
. . . . 5
⊢
((♯‘𝑊) =
3 → 1 ∈ (0..^(♯‘𝑊))) |
13 | | wrdsymbcl 14477 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 1 ∈ (0..^(♯‘𝑊))) → (𝑊‘1) ∈ 𝑉) |
14 | 12, 13 | sylan2 594 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) → (𝑊‘1) ∈ 𝑉) |
15 | | 2ex 12289 |
. . . . . . . 8
⊢ 2 ∈
V |
16 | 15 | tpid3 4778 |
. . . . . . 7
⊢ 2 ∈
{0, 1, 2} |
17 | 16, 3 | eleqtrri 2833 |
. . . . . 6
⊢ 2 ∈
(0..^3) |
18 | 17, 5 | eleqtrrid 2841 |
. . . . 5
⊢
((♯‘𝑊) =
3 → 2 ∈ (0..^(♯‘𝑊))) |
19 | | wrdsymbcl 14477 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0..^(♯‘𝑊))) → (𝑊‘2) ∈ 𝑉) |
20 | 18, 19 | sylan2 594 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) → (𝑊‘2) ∈ 𝑉) |
21 | | simpr 486 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) → (♯‘𝑊) = 3) |
22 | | eqid 2733 |
. . . . . 6
⊢ (𝑊‘0) = (𝑊‘0) |
23 | | eqid 2733 |
. . . . . 6
⊢ (𝑊‘1) = (𝑊‘1) |
24 | | eqid 2733 |
. . . . . 6
⊢ (𝑊‘2) = (𝑊‘2) |
25 | 22, 23, 24 | 3pm3.2i 1340 |
. . . . 5
⊢ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = (𝑊‘2)) |
26 | 21, 25 | jctir 522 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) → ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = (𝑊‘2)))) |
27 | | eqeq2 2745 |
. . . . . . 7
⊢ (𝑎 = (𝑊‘0) → ((𝑊‘0) = 𝑎 ↔ (𝑊‘0) = (𝑊‘0))) |
28 | 27 | 3anbi1d 1441 |
. . . . . 6
⊢ (𝑎 = (𝑊‘0) → (((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐) ↔ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐))) |
29 | 28 | anbi2d 630 |
. . . . 5
⊢ (𝑎 = (𝑊‘0) → (((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)) ↔ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)))) |
30 | | eqeq2 2745 |
. . . . . . 7
⊢ (𝑏 = (𝑊‘1) → ((𝑊‘1) = 𝑏 ↔ (𝑊‘1) = (𝑊‘1))) |
31 | 30 | 3anbi2d 1442 |
. . . . . 6
⊢ (𝑏 = (𝑊‘1) → (((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐) ↔ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = 𝑐))) |
32 | 31 | anbi2d 630 |
. . . . 5
⊢ (𝑏 = (𝑊‘1) → (((♯‘𝑊) = 3 ∧ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)) ↔ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = 𝑐)))) |
33 | | eqeq2 2745 |
. . . . . . 7
⊢ (𝑐 = (𝑊‘2) → ((𝑊‘2) = 𝑐 ↔ (𝑊‘2) = (𝑊‘2))) |
34 | 33 | 3anbi3d 1443 |
. . . . . 6
⊢ (𝑐 = (𝑊‘2) → (((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = 𝑐) ↔ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = (𝑊‘2)))) |
35 | 34 | anbi2d 630 |
. . . . 5
⊢ (𝑐 = (𝑊‘2) → (((♯‘𝑊) = 3 ∧ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = 𝑐)) ↔ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = (𝑊‘2))))) |
36 | 29, 32, 35 | rspc3ev 3629 |
. . . 4
⊢ ((((𝑊‘0) ∈ 𝑉 ∧ (𝑊‘1) ∈ 𝑉 ∧ (𝑊‘2) ∈ 𝑉) ∧ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = (𝑊‘2)))) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐))) |
37 | 8, 14, 20, 26, 36 | syl31anc 1374 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐))) |
38 | | df-3an 1090 |
. . . . . . . . 9
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ↔ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉)) |
39 | | eqwrds3 14912 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ↔ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)))) |
40 | 39 | ex 414 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝑉 → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ↔ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐))))) |
41 | 38, 40 | biimtrrid 242 |
. . . . . . . 8
⊢ (𝑊 ∈ Word 𝑉 → (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉) → (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ↔ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐))))) |
42 | 41 | expd 417 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝑉 → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (𝑐 ∈ 𝑉 → (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ↔ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)))))) |
43 | 42 | adantr 482 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (𝑐 ∈ 𝑉 → (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ↔ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)))))) |
44 | 43 | imp31 419 |
. . . . 5
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑐 ∈ 𝑉) → (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ↔ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)))) |
45 | 44 | rexbidva 3177 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (∃𝑐 ∈ 𝑉 𝑊 = ⟨“𝑎𝑏𝑐”⟩ ↔ ∃𝑐 ∈ 𝑉 ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)))) |
46 | 45 | 2rexbidva 3218 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) → (∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 = ⟨“𝑎𝑏𝑐”⟩ ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)))) |
47 | 37, 46 | mpbird 257 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 = ⟨“𝑎𝑏𝑐”⟩) |
48 | | s3cl 14830 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → ⟨“𝑎𝑏𝑐”⟩ ∈ Word 𝑉) |
49 | 48 | ad4ant123 1173 |
. . . . . 6
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → ⟨“𝑎𝑏𝑐”⟩ ∈ Word 𝑉) |
50 | | s3len 14845 |
. . . . . 6
⊢
(♯‘⟨“𝑎𝑏𝑐”⟩) = 3 |
51 | 49, 50 | jctir 522 |
. . . . 5
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → (⟨“𝑎𝑏𝑐”⟩ ∈ Word 𝑉 ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = 3)) |
52 | | eleq1 2822 |
. . . . . . 7
⊢ (𝑊 = ⟨“𝑎𝑏𝑐”⟩ → (𝑊 ∈ Word 𝑉 ↔ ⟨“𝑎𝑏𝑐”⟩ ∈ Word 𝑉)) |
53 | | fveqeq2 6901 |
. . . . . . 7
⊢ (𝑊 = ⟨“𝑎𝑏𝑐”⟩ → ((♯‘𝑊) = 3 ↔
(♯‘⟨“𝑎𝑏𝑐”⟩) = 3)) |
54 | 52, 53 | anbi12d 632 |
. . . . . 6
⊢ (𝑊 = ⟨“𝑎𝑏𝑐”⟩ → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) ↔ (⟨“𝑎𝑏𝑐”⟩ ∈ Word 𝑉 ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = 3))) |
55 | 54 | adantl 483 |
. . . . 5
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) ↔ (⟨“𝑎𝑏𝑐”⟩ ∈ Word 𝑉 ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = 3))) |
56 | 51, 55 | mpbird 257 |
. . . 4
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3)) |
57 | 56 | rexlimdva2 3158 |
. . 3
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (∃𝑐 ∈ 𝑉 𝑊 = ⟨“𝑎𝑏𝑐”⟩ → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3))) |
58 | 57 | rexlimivv 3200 |
. 2
⊢
(∃𝑎 ∈
𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 = ⟨“𝑎𝑏𝑐”⟩ → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3)) |
59 | 47, 58 | impbii 208 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 = ⟨“𝑎𝑏𝑐”⟩) |