Proof of Theorem s4prop
Step | Hyp | Ref
| Expression |
1 | | df-s4 13595 |
. 2
⊢
〈“𝐴𝐵𝐶𝐷”〉 = (〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉) |
2 | | simpl 473 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → 𝐴 ∈ 𝑆) |
3 | 2 | adantr 481 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → 𝐴 ∈ 𝑆) |
4 | | simpr 477 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → 𝐵 ∈ 𝑆) |
5 | 4 | adantr 481 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → 𝐵 ∈ 𝑆) |
6 | | simpl 473 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → 𝐶 ∈ 𝑆) |
7 | 6 | adantl 482 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → 𝐶 ∈ 𝑆) |
8 | 3, 5, 7 | s3cld 13617 |
. . . . 5
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → 〈“𝐴𝐵𝐶”〉 ∈ Word 𝑆) |
9 | | simpr 477 |
. . . . . 6
⊢ ((𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → 𝐷 ∈ 𝑆) |
10 | 9 | adantl 482 |
. . . . 5
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → 𝐷 ∈ 𝑆) |
11 | | cats1un 13475 |
. . . . 5
⊢
((〈“𝐴𝐵𝐶”〉 ∈ Word 𝑆 ∧ 𝐷 ∈ 𝑆) → (〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉) =
(〈“𝐴𝐵𝐶”〉 ∪
{〈(#‘〈“𝐴𝐵𝐶”〉), 𝐷〉})) |
12 | 8, 10, 11 | syl2anc 693 |
. . . 4
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉) =
(〈“𝐴𝐵𝐶”〉 ∪
{〈(#‘〈“𝐴𝐵𝐶”〉), 𝐷〉})) |
13 | | df-s3 13594 |
. . . . . . 7
⊢
〈“𝐴𝐵𝐶”〉 = (〈“𝐴𝐵”〉 ++ 〈“𝐶”〉) |
14 | | s2cl 13623 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → 〈“𝐴𝐵”〉 ∈ Word 𝑆) |
15 | 14 | adantr 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → 〈“𝐴𝐵”〉 ∈ Word 𝑆) |
16 | | cats1un 13475 |
. . . . . . . 8
⊢
((〈“𝐴𝐵”〉 ∈ Word 𝑆 ∧ 𝐶 ∈ 𝑆) → (〈“𝐴𝐵”〉 ++ 〈“𝐶”〉) =
(〈“𝐴𝐵”〉 ∪
{〈(#‘〈“𝐴𝐵”〉), 𝐶〉})) |
17 | 15, 7, 16 | syl2anc 693 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (〈“𝐴𝐵”〉 ++ 〈“𝐶”〉) =
(〈“𝐴𝐵”〉 ∪
{〈(#‘〈“𝐴𝐵”〉), 𝐶〉})) |
18 | 13, 17 | syl5eq 2668 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → 〈“𝐴𝐵𝐶”〉 = (〈“𝐴𝐵”〉 ∪
{〈(#‘〈“𝐴𝐵”〉), 𝐶〉})) |
19 | | s2prop 13652 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → 〈“𝐴𝐵”〉 = {〈0, 𝐴〉, 〈1, 𝐵〉}) |
20 | 19 | adantr 481 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → 〈“𝐴𝐵”〉 = {〈0, 𝐴〉, 〈1, 𝐵〉}) |
21 | 20 | uneq1d 3766 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (〈“𝐴𝐵”〉 ∪
{〈(#‘〈“𝐴𝐵”〉), 𝐶〉}) = ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪
{〈(#‘〈“𝐴𝐵”〉), 𝐶〉})) |
22 | 18, 21 | eqtrd 2656 |
. . . . 5
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → 〈“𝐴𝐵𝐶”〉 = ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪
{〈(#‘〈“𝐴𝐵”〉), 𝐶〉})) |
23 | 22 | uneq1d 3766 |
. . . 4
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (〈“𝐴𝐵𝐶”〉 ∪
{〈(#‘〈“𝐴𝐵𝐶”〉), 𝐷〉}) = (({〈0, 𝐴〉, 〈1, 𝐵〉} ∪
{〈(#‘〈“𝐴𝐵”〉), 𝐶〉}) ∪
{〈(#‘〈“𝐴𝐵𝐶”〉), 𝐷〉})) |
24 | 12, 23 | eqtrd 2656 |
. . 3
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉) = (({〈0,
𝐴〉, 〈1, 𝐵〉} ∪
{〈(#‘〈“𝐴𝐵”〉), 𝐶〉}) ∪
{〈(#‘〈“𝐴𝐵𝐶”〉), 𝐷〉})) |
25 | | unass 3770 |
. . . 4
⊢
(({〈0, 𝐴〉,
〈1, 𝐵〉} ∪
{〈(#‘〈“𝐴𝐵”〉), 𝐶〉}) ∪
{〈(#‘〈“𝐴𝐵𝐶”〉), 𝐷〉}) = ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪
({〈(#‘〈“𝐴𝐵”〉), 𝐶〉} ∪
{〈(#‘〈“𝐴𝐵𝐶”〉), 𝐷〉})) |
26 | 25 | a1i 11 |
. . 3
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (({〈0, 𝐴〉, 〈1, 𝐵〉} ∪
{〈(#‘〈“𝐴𝐵”〉), 𝐶〉}) ∪
{〈(#‘〈“𝐴𝐵𝐶”〉), 𝐷〉}) = ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪
({〈(#‘〈“𝐴𝐵”〉), 𝐶〉} ∪
{〈(#‘〈“𝐴𝐵𝐶”〉), 𝐷〉}))) |
27 | | df-pr 4180 |
. . . . 5
⊢
{〈(#‘〈“𝐴𝐵”〉), 𝐶〉, 〈(#‘〈“𝐴𝐵𝐶”〉), 𝐷〉} =
({〈(#‘〈“𝐴𝐵”〉), 𝐶〉} ∪
{〈(#‘〈“𝐴𝐵𝐶”〉), 𝐷〉}) |
28 | | s2len 13634 |
. . . . . . . 8
⊢
(#‘〈“𝐴𝐵”〉) = 2 |
29 | 28 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (#‘〈“𝐴𝐵”〉) = 2) |
30 | 29 | opeq1d 4408 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → 〈(#‘〈“𝐴𝐵”〉), 𝐶〉 = 〈2, 𝐶〉) |
31 | | s3len 13639 |
. . . . . . . 8
⊢
(#‘〈“𝐴𝐵𝐶”〉) = 3 |
32 | 31 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (#‘〈“𝐴𝐵𝐶”〉) = 3) |
33 | 32 | opeq1d 4408 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → 〈(#‘〈“𝐴𝐵𝐶”〉), 𝐷〉 = 〈3, 𝐷〉) |
34 | 30, 33 | preq12d 4276 |
. . . . 5
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → {〈(#‘〈“𝐴𝐵”〉), 𝐶〉, 〈(#‘〈“𝐴𝐵𝐶”〉), 𝐷〉} = {〈2, 𝐶〉, 〈3, 𝐷〉}) |
35 | 27, 34 | syl5eqr 2670 |
. . . 4
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) →
({〈(#‘〈“𝐴𝐵”〉), 𝐶〉} ∪
{〈(#‘〈“𝐴𝐵𝐶”〉), 𝐷〉}) = {〈2, 𝐶〉, 〈3, 𝐷〉}) |
36 | 35 | uneq2d 3767 |
. . 3
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪
({〈(#‘〈“𝐴𝐵”〉), 𝐶〉} ∪
{〈(#‘〈“𝐴𝐵𝐶”〉), 𝐷〉})) = ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐷〉})) |
37 | 24, 26, 36 | 3eqtrd 2660 |
. 2
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉) = ({〈0,
𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐷〉})) |
38 | 1, 37 | syl5eq 2668 |
1
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → 〈“𝐴𝐵𝐶𝐷”〉 = ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐷〉})) |