Proof of Theorem wrdl3s3
| Step | Hyp | Ref
| Expression |
| 1 | | c0ex 11255 |
. . . . . . . 8
⊢ 0 ∈
V |
| 2 | 1 | tpid1 4768 |
. . . . . . 7
⊢ 0 ∈
{0, 1, 2} |
| 3 | | fzo0to3tp 13791 |
. . . . . . 7
⊢ (0..^3) =
{0, 1, 2} |
| 4 | 2, 3 | eleqtrri 2840 |
. . . . . 6
⊢ 0 ∈
(0..^3) |
| 5 | | oveq2 7439 |
. . . . . 6
⊢
((♯‘𝑊) =
3 → (0..^(♯‘𝑊)) = (0..^3)) |
| 6 | 4, 5 | eleqtrrid 2848 |
. . . . 5
⊢
((♯‘𝑊) =
3 → 0 ∈ (0..^(♯‘𝑊))) |
| 7 | | wrdsymbcl 14565 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 0 ∈ (0..^(♯‘𝑊))) → (𝑊‘0) ∈ 𝑉) |
| 8 | 6, 7 | sylan2 593 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) → (𝑊‘0) ∈ 𝑉) |
| 9 | | 1ex 11257 |
. . . . . . . 8
⊢ 1 ∈
V |
| 10 | 9 | tpid2 4770 |
. . . . . . 7
⊢ 1 ∈
{0, 1, 2} |
| 11 | 10, 3 | eleqtrri 2840 |
. . . . . 6
⊢ 1 ∈
(0..^3) |
| 12 | 11, 5 | eleqtrrid 2848 |
. . . . 5
⊢
((♯‘𝑊) =
3 → 1 ∈ (0..^(♯‘𝑊))) |
| 13 | | wrdsymbcl 14565 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 1 ∈ (0..^(♯‘𝑊))) → (𝑊‘1) ∈ 𝑉) |
| 14 | 12, 13 | sylan2 593 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) → (𝑊‘1) ∈ 𝑉) |
| 15 | | 2ex 12343 |
. . . . . . . 8
⊢ 2 ∈
V |
| 16 | 15 | tpid3 4773 |
. . . . . . 7
⊢ 2 ∈
{0, 1, 2} |
| 17 | 16, 3 | eleqtrri 2840 |
. . . . . 6
⊢ 2 ∈
(0..^3) |
| 18 | 17, 5 | eleqtrrid 2848 |
. . . . 5
⊢
((♯‘𝑊) =
3 → 2 ∈ (0..^(♯‘𝑊))) |
| 19 | | wrdsymbcl 14565 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0..^(♯‘𝑊))) → (𝑊‘2) ∈ 𝑉) |
| 20 | 18, 19 | sylan2 593 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) → (𝑊‘2) ∈ 𝑉) |
| 21 | | simpr 484 |
. . . . 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 1340 |
. . . . 5
⊢ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = (𝑊‘2)) |
| 26 | 21, 25 | jctir 520 |
. . . 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 630 |
. . . . 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 630 |
. . . . 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 630 |
. . . . 5
⊢ (𝑐 = (𝑊‘2) → (((♯‘𝑊) = 3 ∧ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = 𝑐)) ↔ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = (𝑊‘0) ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = (𝑊‘2))))) |
| 36 | 29, 32, 35 | rspc3ev 3639 |
. . . 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 1089 |
. . . . . . . . 9
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ↔ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉)) |
| 39 | | eqwrds3 15000 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑊 = 〈“𝑎𝑏𝑐”〉 ↔ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)))) |
| 40 | 39 | ex 412 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝑉 → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → (𝑊 = 〈“𝑎𝑏𝑐”〉 ↔ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐))))) |
| 41 | 38, 40 | biimtrrid 243 |
. . . . . . . 8
⊢ (𝑊 ∈ Word 𝑉 → (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉) → (𝑊 = 〈“𝑎𝑏𝑐”〉 ↔ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐))))) |
| 42 | 41 | expd 415 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝑉 → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (𝑐 ∈ 𝑉 → (𝑊 = 〈“𝑎𝑏𝑐”〉 ↔ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)))))) |
| 43 | 42 | adantr 480 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (𝑐 ∈ 𝑉 → (𝑊 = 〈“𝑎𝑏𝑐”〉 ↔ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)))))) |
| 44 | 43 | imp31 417 |
. . . . 5
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑐 ∈ 𝑉) → (𝑊 = 〈“𝑎𝑏𝑐”〉 ↔ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)))) |
| 45 | 44 | rexbidva 3177 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (∃𝑐 ∈ 𝑉 𝑊 = 〈“𝑎𝑏𝑐”〉 ↔ ∃𝑐 ∈ 𝑉 ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)))) |
| 46 | 45 | 2rexbidva 3220 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) → (∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 = 〈“𝑎𝑏𝑐”〉 ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘1) = 𝑏 ∧ (𝑊‘2) = 𝑐)))) |
| 47 | 37, 46 | mpbird 257 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 = 〈“𝑎𝑏𝑐”〉) |
| 48 | | s3cl 14918 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → 〈“𝑎𝑏𝑐”〉 ∈ Word 𝑉) |
| 49 | 48 | ad4ant123 1173 |
. . . . . 6
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → 〈“𝑎𝑏𝑐”〉 ∈ Word 𝑉) |
| 50 | | s3len 14933 |
. . . . . 6
⊢
(♯‘〈“𝑎𝑏𝑐”〉) = 3 |
| 51 | 49, 50 | jctir 520 |
. . . . 5
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → (〈“𝑎𝑏𝑐”〉 ∈ Word 𝑉 ∧ (♯‘〈“𝑎𝑏𝑐”〉) = 3)) |
| 52 | | eleq1 2829 |
. . . . . . 7
⊢ (𝑊 = 〈“𝑎𝑏𝑐”〉 → (𝑊 ∈ Word 𝑉 ↔ 〈“𝑎𝑏𝑐”〉 ∈ Word 𝑉)) |
| 53 | | fveqeq2 6915 |
. . . . . . 7
⊢ (𝑊 = 〈“𝑎𝑏𝑐”〉 → ((♯‘𝑊) = 3 ↔
(♯‘〈“𝑎𝑏𝑐”〉) = 3)) |
| 54 | 52, 53 | anbi12d 632 |
. . . . . 6
⊢ (𝑊 = 〈“𝑎𝑏𝑐”〉 → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) ↔ (〈“𝑎𝑏𝑐”〉 ∈ Word 𝑉 ∧ (♯‘〈“𝑎𝑏𝑐”〉) = 3))) |
| 55 | 54 | adantl 481 |
. . . . 5
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) ↔ (〈“𝑎𝑏𝑐”〉 ∈ Word 𝑉 ∧ (♯‘〈“𝑎𝑏𝑐”〉) = 3))) |
| 56 | 51, 55 | mpbird 257 |
. . . 4
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3)) |
| 57 | 56 | rexlimdva2 3157 |
. . 3
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (∃𝑐 ∈ 𝑉 𝑊 = 〈“𝑎𝑏𝑐”〉 → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3))) |
| 58 | 57 | rexlimivv 3201 |
. 2
⊢
(∃𝑎 ∈
𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 = 〈“𝑎𝑏𝑐”〉 → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3)) |
| 59 | 47, 58 | impbii 209 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 = 〈“𝑎𝑏𝑐”〉) |