Proof of Theorem wrdl3s3
Step | Hyp | Ref
| Expression |
1 | | c0ex 10827 |
. . . . . . . 8
⊢ 0 ∈
V |
2 | 1 | tpid1 4684 |
. . . . . . 7
⊢ 0 ∈
{0, 1, 2} |
3 | | fzo0to3tp 13328 |
. . . . . . 7
⊢ (0..^3) =
{0, 1, 2} |
4 | 2, 3 | eleqtrri 2837 |
. . . . . 6
⊢ 0 ∈
(0..^3) |
5 | | oveq2 7221 |
. . . . . 6
⊢
((♯‘𝑊) =
3 → (0..^(♯‘𝑊)) = (0..^3)) |
6 | 4, 5 | eleqtrrid 2845 |
. . . . 5
⊢
((♯‘𝑊) =
3 → 0 ∈ (0..^(♯‘𝑊))) |
7 | | wrdsymbcl 14082 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 0 ∈ (0..^(♯‘𝑊))) → (𝑊‘0) ∈ 𝑉) |
8 | 6, 7 | sylan2 596 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) → (𝑊‘0) ∈ 𝑉) |
9 | | 1ex 10829 |
. . . . . . . 8
⊢ 1 ∈
V |
10 | 9 | tpid2 4686 |
. . . . . . 7
⊢ 1 ∈
{0, 1, 2} |
11 | 10, 3 | eleqtrri 2837 |
. . . . . 6
⊢ 1 ∈
(0..^3) |
12 | 11, 5 | eleqtrrid 2845 |
. . . . 5
⊢
((♯‘𝑊) =
3 → 1 ∈ (0..^(♯‘𝑊))) |
13 | | wrdsymbcl 14082 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 1 ∈ (0..^(♯‘𝑊))) → (𝑊‘1) ∈ 𝑉) |
14 | 12, 13 | sylan2 596 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) → (𝑊‘1) ∈ 𝑉) |
15 | | 2ex 11907 |
. . . . . . . 8
⊢ 2 ∈
V |
16 | 15 | tpid3 4689 |
. . . . . . 7
⊢ 2 ∈
{0, 1, 2} |
17 | 16, 3 | eleqtrri 2837 |
. . . . . 6
⊢ 2 ∈
(0..^3) |
18 | 17, 5 | eleqtrrid 2845 |
. . . . 5
⊢
((♯‘𝑊) =
3 → 2 ∈ (0..^(♯‘𝑊))) |
19 | | wrdsymbcl 14082 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0..^(♯‘𝑊))) → (𝑊‘2) ∈ 𝑉) |
20 | 18, 19 | sylan2 596 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) → (𝑊‘2) ∈ 𝑉) |
21 | | simpr 488 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) → (♯‘𝑊) = 3) |
22 | | eqid 2737 |
. . . . . 6
⊢ (𝑊‘0) = (𝑊‘0) |
23 | | eqid 2737 |
. . . . . 6
⊢ (𝑊‘1) = (𝑊‘1) |
24 | | eqid 2737 |
. . . . . 6
⊢ (𝑊‘2) = (𝑊‘2) |
25 | 22, 23, 24 | 3pm3.2i 1341 |
. . . . 5
⊢ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = (𝑊‘2)) |
26 | 21, 25 | jctir 524 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) → ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = (𝑊‘2)))) |
27 | | eqeq2 2749 |
. . . . . . 7
⊢ (𝑎 = (𝑊‘0) → ((𝑊‘0) = 𝑎 ↔ (𝑊‘0) = (𝑊‘0))) |
28 | 27 | 3anbi1d 1442 |
. . . . . 6
⊢ (𝑎 = (𝑊‘0) → (((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐) ↔ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐))) |
29 | 28 | anbi2d 632 |
. . . . 5
⊢ (𝑎 = (𝑊‘0) → (((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)) ↔ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)))) |
30 | | eqeq2 2749 |
. . . . . . 7
⊢ (𝑏 = (𝑊‘1) → ((𝑊‘1) = 𝑏 ↔ (𝑊‘1) = (𝑊‘1))) |
31 | 30 | 3anbi2d 1443 |
. . . . . 6
⊢ (𝑏 = (𝑊‘1) → (((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐) ↔ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = 𝑐))) |
32 | 31 | anbi2d 632 |
. . . . 5
⊢ (𝑏 = (𝑊‘1) → (((♯‘𝑊) = 3 ∧ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)) ↔ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = 𝑐)))) |
33 | | eqeq2 2749 |
. . . . . . 7
⊢ (𝑐 = (𝑊‘2) → ((𝑊‘2) = 𝑐 ↔ (𝑊‘2) = (𝑊‘2))) |
34 | 33 | 3anbi3d 1444 |
. . . . . 6
⊢ (𝑐 = (𝑊‘2) → (((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = 𝑐) ↔ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = (𝑊‘2)))) |
35 | 34 | anbi2d 632 |
. . . . 5
⊢ (𝑐 = (𝑊‘2) → (((♯‘𝑊) = 3 ∧ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = 𝑐)) ↔ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = (𝑊‘2))))) |
36 | 29, 32, 35 | rspc3ev 3551 |
. . . 4
⊢ ((((𝑊‘0) ∈ 𝑉 ∧ (𝑊‘1) ∈ 𝑉 ∧ (𝑊‘2) ∈ 𝑉) ∧ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = (𝑊‘2)))) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐))) |
37 | 8, 14, 20, 26, 36 | syl31anc 1375 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐))) |
38 | | df-3an 1091 |
. . . . . . . . 9
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ↔ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉)) |
39 | | eqwrds3 14528 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑊 = 〈“𝑎𝑏𝑐”〉 ↔ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)))) |
40 | 39 | ex 416 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝑉 → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → (𝑊 = 〈“𝑎𝑏𝑐”〉 ↔ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐))))) |
41 | 38, 40 | syl5bir 246 |
. . . . . . . 8
⊢ (𝑊 ∈ Word 𝑉 → (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉) → (𝑊 = 〈“𝑎𝑏𝑐”〉 ↔ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐))))) |
42 | 41 | expd 419 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝑉 → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (𝑐 ∈ 𝑉 → (𝑊 = 〈“𝑎𝑏𝑐”〉 ↔ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)))))) |
43 | 42 | adantr 484 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (𝑐 ∈ 𝑉 → (𝑊 = 〈“𝑎𝑏𝑐”〉 ↔ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)))))) |
44 | 43 | imp31 421 |
. . . . 5
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑐 ∈ 𝑉) → (𝑊 = 〈“𝑎𝑏𝑐”〉 ↔ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)))) |
45 | 44 | rexbidva 3215 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (∃𝑐 ∈ 𝑉 𝑊 = 〈“𝑎𝑏𝑐”〉 ↔ ∃𝑐 ∈ 𝑉 ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)))) |
46 | 45 | 2rexbidva 3218 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) → (∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 = 〈“𝑎𝑏𝑐”〉 ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)))) |
47 | 37, 46 | mpbird 260 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 = 〈“𝑎𝑏𝑐”〉) |
48 | | s3cl 14444 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → 〈“𝑎𝑏𝑐”〉 ∈ Word 𝑉) |
49 | 48 | ad4ant123 1174 |
. . . . . 6
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → 〈“𝑎𝑏𝑐”〉 ∈ Word 𝑉) |
50 | | s3len 14459 |
. . . . . 6
⊢
(♯‘〈“𝑎𝑏𝑐”〉) = 3 |
51 | 49, 50 | jctir 524 |
. . . . 5
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → (〈“𝑎𝑏𝑐”〉 ∈ Word 𝑉 ∧ (♯‘〈“𝑎𝑏𝑐”〉) = 3)) |
52 | | eleq1 2825 |
. . . . . . 7
⊢ (𝑊 = 〈“𝑎𝑏𝑐”〉 → (𝑊 ∈ Word 𝑉 ↔ 〈“𝑎𝑏𝑐”〉 ∈ Word 𝑉)) |
53 | | fveqeq2 6726 |
. . . . . . 7
⊢ (𝑊 = 〈“𝑎𝑏𝑐”〉 → ((♯‘𝑊) = 3 ↔
(♯‘〈“𝑎𝑏𝑐”〉) = 3)) |
54 | 52, 53 | anbi12d 634 |
. . . . . 6
⊢ (𝑊 = 〈“𝑎𝑏𝑐”〉 → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) ↔ (〈“𝑎𝑏𝑐”〉 ∈ Word 𝑉 ∧ (♯‘〈“𝑎𝑏𝑐”〉) = 3))) |
55 | 54 | adantl 485 |
. . . . 5
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) ↔ (〈“𝑎𝑏𝑐”〉 ∈ Word 𝑉 ∧ (♯‘〈“𝑎𝑏𝑐”〉) = 3))) |
56 | 51, 55 | mpbird 260 |
. . . 4
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3)) |
57 | 56 | rexlimdva2 3206 |
. . 3
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (∃𝑐 ∈ 𝑉 𝑊 = 〈“𝑎𝑏𝑐”〉 → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3))) |
58 | 57 | rexlimivv 3211 |
. 2
⊢
(∃𝑎 ∈
𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 = 〈“𝑎𝑏𝑐”〉 → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3)) |
59 | 47, 58 | impbii 212 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 = 〈“𝑎𝑏𝑐”〉) |