Proof of Theorem wrdl3s3
Step | Hyp | Ref
| Expression |
1 | | c0ex 9913 |
. . . . . . . 8
⊢ 0 ∈
V |
2 | 1 | tpid1 4246 |
. . . . . . 7
⊢ 0 ∈
{0, 1, 2} |
3 | | fzo0to3tp 12421 |
. . . . . . 7
⊢ (0..^3) =
{0, 1, 2} |
4 | 2, 3 | eleqtrri 2687 |
. . . . . 6
⊢ 0 ∈
(0..^3) |
5 | | oveq2 6557 |
. . . . . 6
⊢
((#‘𝑊) = 3
→ (0..^(#‘𝑊)) =
(0..^3)) |
6 | 4, 5 | syl5eleqr 2695 |
. . . . 5
⊢
((#‘𝑊) = 3
→ 0 ∈ (0..^(#‘𝑊))) |
7 | | wrdsymbcl 13173 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 0 ∈ (0..^(#‘𝑊))) → (𝑊‘0) ∈ 𝑉) |
8 | 6, 7 | sylan2 490 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 3) → (𝑊‘0) ∈ 𝑉) |
9 | | 1ex 9914 |
. . . . . . . 8
⊢ 1 ∈
V |
10 | 9 | tpid2 4247 |
. . . . . . 7
⊢ 1 ∈
{0, 1, 2} |
11 | 10, 3 | eleqtrri 2687 |
. . . . . 6
⊢ 1 ∈
(0..^3) |
12 | 11, 5 | syl5eleqr 2695 |
. . . . 5
⊢
((#‘𝑊) = 3
→ 1 ∈ (0..^(#‘𝑊))) |
13 | | wrdsymbcl 13173 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 1 ∈ (0..^(#‘𝑊))) → (𝑊‘1) ∈ 𝑉) |
14 | 12, 13 | sylan2 490 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 3) → (𝑊‘1) ∈ 𝑉) |
15 | | 2ex 10969 |
. . . . . . . 8
⊢ 2 ∈
V |
16 | 15 | tpid3 4250 |
. . . . . . 7
⊢ 2 ∈
{0, 1, 2} |
17 | 16, 3 | eleqtrri 2687 |
. . . . . 6
⊢ 2 ∈
(0..^3) |
18 | 17, 5 | syl5eleqr 2695 |
. . . . 5
⊢
((#‘𝑊) = 3
→ 2 ∈ (0..^(#‘𝑊))) |
19 | | wrdsymbcl 13173 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0..^(#‘𝑊))) → (𝑊‘2) ∈ 𝑉) |
20 | 18, 19 | sylan2 490 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 3) → (𝑊‘2) ∈ 𝑉) |
21 | | simpr 476 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 3) → (#‘𝑊) = 3) |
22 | | eqid 2610 |
. . . . . 6
⊢ (𝑊‘0) = (𝑊‘0) |
23 | | eqid 2610 |
. . . . . 6
⊢ (𝑊‘1) = (𝑊‘1) |
24 | | eqid 2610 |
. . . . . 6
⊢ (𝑊‘2) = (𝑊‘2) |
25 | 22, 23, 24 | 3pm3.2i 1232 |
. . . . 5
⊢ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = (𝑊‘2)) |
26 | 21, 25 | jctir 559 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 3) → ((#‘𝑊) = 3 ∧ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = (𝑊‘2)))) |
27 | | eqeq2 2621 |
. . . . . . 7
⊢ (𝑎 = (𝑊‘0) → ((𝑊‘0) = 𝑎 ↔ (𝑊‘0) = (𝑊‘0))) |
28 | 27 | 3anbi1d 1395 |
. . . . . 6
⊢ (𝑎 = (𝑊‘0) → (((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐) ↔ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐))) |
29 | 28 | anbi2d 736 |
. . . . 5
⊢ (𝑎 = (𝑊‘0) → (((#‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)) ↔ ((#‘𝑊) = 3 ∧ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)))) |
30 | | eqeq2 2621 |
. . . . . . 7
⊢ (𝑏 = (𝑊‘1) → ((𝑊‘1) = 𝑏 ↔ (𝑊‘1) = (𝑊‘1))) |
31 | 30 | 3anbi2d 1396 |
. . . . . 6
⊢ (𝑏 = (𝑊‘1) → (((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐) ↔ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = 𝑐))) |
32 | 31 | anbi2d 736 |
. . . . 5
⊢ (𝑏 = (𝑊‘1) → (((#‘𝑊) = 3 ∧ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)) ↔ ((#‘𝑊) = 3 ∧ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = 𝑐)))) |
33 | | eqeq2 2621 |
. . . . . . 7
⊢ (𝑐 = (𝑊‘2) → ((𝑊‘2) = 𝑐 ↔ (𝑊‘2) = (𝑊‘2))) |
34 | 33 | 3anbi3d 1397 |
. . . . . 6
⊢ (𝑐 = (𝑊‘2) → (((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = 𝑐) ↔ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = (𝑊‘2)))) |
35 | 34 | anbi2d 736 |
. . . . 5
⊢ (𝑐 = (𝑊‘2) → (((#‘𝑊) = 3 ∧ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = 𝑐)) ↔ ((#‘𝑊) = 3 ∧ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = (𝑊‘2))))) |
36 | 29, 32, 35 | rspc3ev 3297 |
. . . 4
⊢ ((((𝑊‘0) ∈ 𝑉 ∧ (𝑊‘1) ∈ 𝑉 ∧ (𝑊‘2) ∈ 𝑉) ∧ ((#‘𝑊) = 3 ∧ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = (𝑊‘2)))) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ((#‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐))) |
37 | 8, 14, 20, 26, 36 | syl31anc 1321 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 3) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ((#‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐))) |
38 | | df-3an 1033 |
. . . . . . . . 9
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ↔ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉)) |
39 | | eqwrds3 13552 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑊 = 〈“𝑎𝑏𝑐”〉 ↔ ((#‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)))) |
40 | 39 | ex 449 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝑉 → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → (𝑊 = 〈“𝑎𝑏𝑐”〉 ↔ ((#‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐))))) |
41 | 38, 40 | syl5bir 232 |
. . . . . . . 8
⊢ (𝑊 ∈ Word 𝑉 → (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉) → (𝑊 = 〈“𝑎𝑏𝑐”〉 ↔ ((#‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐))))) |
42 | 41 | expd 451 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝑉 → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (𝑐 ∈ 𝑉 → (𝑊 = 〈“𝑎𝑏𝑐”〉 ↔ ((#‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)))))) |
43 | 42 | adantr 480 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 3) → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (𝑐 ∈ 𝑉 → (𝑊 = 〈“𝑎𝑏𝑐”〉 ↔ ((#‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)))))) |
44 | 43 | imp31 447 |
. . . . 5
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 3) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑐 ∈ 𝑉) → (𝑊 = 〈“𝑎𝑏𝑐”〉 ↔ ((#‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)))) |
45 | 44 | rexbidva 3031 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 3) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (∃𝑐 ∈ 𝑉 𝑊 = 〈“𝑎𝑏𝑐”〉 ↔ ∃𝑐 ∈ 𝑉 ((#‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)))) |
46 | 45 | 2rexbidva 3038 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 3) → (∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 = 〈“𝑎𝑏𝑐”〉 ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ((#‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)))) |
47 | 37, 46 | mpbird 246 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 3) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 = 〈“𝑎𝑏𝑐”〉) |
48 | | s3cl 13474 |
. . . . . . . 8
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → 〈“𝑎𝑏𝑐”〉 ∈ Word 𝑉) |
49 | 48 | ad4ant123 1286 |
. . . . . . 7
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → 〈“𝑎𝑏𝑐”〉 ∈ Word 𝑉) |
50 | | s3len 13489 |
. . . . . . 7
⊢
(#‘〈“𝑎𝑏𝑐”〉) = 3 |
51 | 49, 50 | jctir 559 |
. . . . . 6
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → (〈“𝑎𝑏𝑐”〉 ∈ Word 𝑉 ∧ (#‘〈“𝑎𝑏𝑐”〉) = 3)) |
52 | | eleq1 2676 |
. . . . . . . 8
⊢ (𝑊 = 〈“𝑎𝑏𝑐”〉 → (𝑊 ∈ Word 𝑉 ↔ 〈“𝑎𝑏𝑐”〉 ∈ Word 𝑉)) |
53 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑊 = 〈“𝑎𝑏𝑐”〉 → (#‘𝑊) = (#‘〈“𝑎𝑏𝑐”〉)) |
54 | 53 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑊 = 〈“𝑎𝑏𝑐”〉 → ((#‘𝑊) = 3 ↔
(#‘〈“𝑎𝑏𝑐”〉) = 3)) |
55 | 52, 54 | anbi12d 743 |
. . . . . . 7
⊢ (𝑊 = 〈“𝑎𝑏𝑐”〉 → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 3) ↔ (〈“𝑎𝑏𝑐”〉 ∈ Word 𝑉 ∧ (#‘〈“𝑎𝑏𝑐”〉) = 3))) |
56 | 55 | adantl 481 |
. . . . . 6
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 3) ↔ (〈“𝑎𝑏𝑐”〉 ∈ Word 𝑉 ∧ (#‘〈“𝑎𝑏𝑐”〉) = 3))) |
57 | 51, 56 | mpbird 246 |
. . . . 5
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 3)) |
58 | 57 | ex 449 |
. . . 4
⊢ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉) → (𝑊 = 〈“𝑎𝑏𝑐”〉 → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 3))) |
59 | 58 | rexlimdva 3013 |
. . 3
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (∃𝑐 ∈ 𝑉 𝑊 = 〈“𝑎𝑏𝑐”〉 → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 3))) |
60 | 59 | rexlimivv 3018 |
. 2
⊢
(∃𝑎 ∈
𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 = 〈“𝑎𝑏𝑐”〉 → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 3)) |
61 | 47, 60 | impbii 198 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 3) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 = 〈“𝑎𝑏𝑐”〉) |