Step | Hyp | Ref
| Expression |
1 | | inss1 4229 |
. . . . . . . . 9
β’
(π« Ο β© Fin) β π« Ο |
2 | 1 | sseli 3979 |
. . . . . . . 8
β’ (π΄ β (π« Ο β©
Fin) β π΄ β
π« Ο) |
3 | 2 | elpwid 4612 |
. . . . . . 7
β’ (π΄ β (π« Ο β©
Fin) β π΄ β
Ο) |
4 | 3 | adantr 480 |
. . . . . 6
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β π΄ β Ο) |
5 | 1 | sseli 3979 |
. . . . . . . 8
β’ (π΅ β (π« Ο β©
Fin) β π΅ β
π« Ο) |
6 | 5 | elpwid 4612 |
. . . . . . 7
β’ (π΅ β (π« Ο β©
Fin) β π΅ β
Ο) |
7 | 6 | adantl 481 |
. . . . . 6
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β π΅ β Ο) |
8 | 4, 7 | unssd 4187 |
. . . . 5
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β (π΄ βͺ π΅) β Ο) |
9 | | inss2 4230 |
. . . . . . 7
β’
(π« Ο β© Fin) β Fin |
10 | 9 | sseli 3979 |
. . . . . 6
β’ (π΄ β (π« Ο β©
Fin) β π΄ β
Fin) |
11 | 9 | sseli 3979 |
. . . . . 6
β’ (π΅ β (π« Ο β©
Fin) β π΅ β
Fin) |
12 | | unfi 9175 |
. . . . . 6
β’ ((π΄ β Fin β§ π΅ β Fin) β (π΄ βͺ π΅) β Fin) |
13 | 10, 11, 12 | syl2an 595 |
. . . . 5
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β (π΄ βͺ π΅) β Fin) |
14 | | nnunifi 9297 |
. . . . 5
β’ (((π΄ βͺ π΅) β Ο β§ (π΄ βͺ π΅) β Fin) β βͺ (π΄
βͺ π΅) β
Ο) |
15 | 8, 13, 14 | syl2anc 583 |
. . . 4
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β βͺ (π΄ βͺ π΅) β Ο) |
16 | | peano2 7884 |
. . . 4
β’ (βͺ (π΄
βͺ π΅) β Ο
β suc βͺ (π΄ βͺ π΅) β Ο) |
17 | 15, 16 | syl 17 |
. . 3
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β suc βͺ (π΄ βͺ π΅) β Ο) |
18 | | ineq2 4207 |
. . . . . . . 8
β’ (π = β
β (π΄ β© π) = (π΄ β© β
)) |
19 | 18 | fveq2d 6896 |
. . . . . . 7
β’ (π = β
β (πΉβ(π΄ β© π)) = (πΉβ(π΄ β© β
))) |
20 | | ineq2 4207 |
. . . . . . . 8
β’ (π = β
β (π΅ β© π) = (π΅ β© β
)) |
21 | 20 | fveq2d 6896 |
. . . . . . 7
β’ (π = β
β (πΉβ(π΅ β© π)) = (πΉβ(π΅ β© β
))) |
22 | 19, 21 | eqeq12d 2747 |
. . . . . 6
β’ (π = β
β ((πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)) β (πΉβ(π΄ β© β
)) = (πΉβ(π΅ β© β
)))) |
23 | 18, 20 | eqeq12d 2747 |
. . . . . 6
β’ (π = β
β ((π΄ β© π) = (π΅ β© π) β (π΄ β© β
) = (π΅ β© β
))) |
24 | 22, 23 | imbi12d 343 |
. . . . 5
β’ (π = β
β (((πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)) β (π΄ β© π) = (π΅ β© π)) β ((πΉβ(π΄ β© β
)) = (πΉβ(π΅ β© β
)) β (π΄ β© β
) = (π΅ β© β
)))) |
25 | 24 | imbi2d 339 |
. . . 4
β’ (π = β
β (((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β ((πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)) β (π΄ β© π) = (π΅ β© π))) β ((π΄ β (π« Ο β© Fin) β§
π΅ β (π« Ο
β© Fin)) β ((πΉβ(π΄ β© β
)) = (πΉβ(π΅ β© β
)) β (π΄ β© β
) = (π΅ β© β
))))) |
26 | | ineq2 4207 |
. . . . . . . 8
β’ (π = π β (π΄ β© π) = (π΄ β© π)) |
27 | 26 | fveq2d 6896 |
. . . . . . 7
β’ (π = π β (πΉβ(π΄ β© π)) = (πΉβ(π΄ β© π))) |
28 | | ineq2 4207 |
. . . . . . . 8
β’ (π = π β (π΅ β© π) = (π΅ β© π)) |
29 | 28 | fveq2d 6896 |
. . . . . . 7
β’ (π = π β (πΉβ(π΅ β© π)) = (πΉβ(π΅ β© π))) |
30 | 27, 29 | eqeq12d 2747 |
. . . . . 6
β’ (π = π β ((πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)) β (πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)))) |
31 | 26, 28 | eqeq12d 2747 |
. . . . . 6
β’ (π = π β ((π΄ β© π) = (π΅ β© π) β (π΄ β© π) = (π΅ β© π))) |
32 | 30, 31 | imbi12d 343 |
. . . . 5
β’ (π = π β (((πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)) β (π΄ β© π) = (π΅ β© π)) β ((πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)) β (π΄ β© π) = (π΅ β© π)))) |
33 | 32 | imbi2d 339 |
. . . 4
β’ (π = π β (((π΄ β (π« Ο β© Fin) β§
π΅ β (π« Ο
β© Fin)) β ((πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)) β (π΄ β© π) = (π΅ β© π))) β ((π΄ β (π« Ο β© Fin) β§
π΅ β (π« Ο
β© Fin)) β ((πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)) β (π΄ β© π) = (π΅ β© π))))) |
34 | | ineq2 4207 |
. . . . . . . 8
β’ (π = suc π β (π΄ β© π) = (π΄ β© suc π)) |
35 | 34 | fveq2d 6896 |
. . . . . . 7
β’ (π = suc π β (πΉβ(π΄ β© π)) = (πΉβ(π΄ β© suc π))) |
36 | | ineq2 4207 |
. . . . . . . 8
β’ (π = suc π β (π΅ β© π) = (π΅ β© suc π)) |
37 | 36 | fveq2d 6896 |
. . . . . . 7
β’ (π = suc π β (πΉβ(π΅ β© π)) = (πΉβ(π΅ β© suc π))) |
38 | 35, 37 | eqeq12d 2747 |
. . . . . 6
β’ (π = suc π β ((πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)) β (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π)))) |
39 | 34, 36 | eqeq12d 2747 |
. . . . . 6
β’ (π = suc π β ((π΄ β© π) = (π΅ β© π) β (π΄ β© suc π) = (π΅ β© suc π))) |
40 | 38, 39 | imbi12d 343 |
. . . . 5
β’ (π = suc π β (((πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)) β (π΄ β© π) = (π΅ β© π)) β ((πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π)) β (π΄ β© suc π) = (π΅ β© suc π)))) |
41 | 40 | imbi2d 339 |
. . . 4
β’ (π = suc π β (((π΄ β (π« Ο β© Fin) β§
π΅ β (π« Ο
β© Fin)) β ((πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)) β (π΄ β© π) = (π΅ β© π))) β ((π΄ β (π« Ο β© Fin) β§
π΅ β (π« Ο
β© Fin)) β ((πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π)) β (π΄ β© suc π) = (π΅ β© suc π))))) |
42 | | ineq2 4207 |
. . . . . . . 8
β’ (π = suc βͺ (π΄
βͺ π΅) β (π΄ β© π) = (π΄ β© suc βͺ
(π΄ βͺ π΅))) |
43 | 42 | fveq2d 6896 |
. . . . . . 7
β’ (π = suc βͺ (π΄
βͺ π΅) β (πΉβ(π΄ β© π)) = (πΉβ(π΄ β© suc βͺ
(π΄ βͺ π΅)))) |
44 | | ineq2 4207 |
. . . . . . . 8
β’ (π = suc βͺ (π΄
βͺ π΅) β (π΅ β© π) = (π΅ β© suc βͺ
(π΄ βͺ π΅))) |
45 | 44 | fveq2d 6896 |
. . . . . . 7
β’ (π = suc βͺ (π΄
βͺ π΅) β (πΉβ(π΅ β© π)) = (πΉβ(π΅ β© suc βͺ
(π΄ βͺ π΅)))) |
46 | 43, 45 | eqeq12d 2747 |
. . . . . 6
β’ (π = suc βͺ (π΄
βͺ π΅) β ((πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)) β (πΉβ(π΄ β© suc βͺ
(π΄ βͺ π΅))) = (πΉβ(π΅ β© suc βͺ
(π΄ βͺ π΅))))) |
47 | 42, 44 | eqeq12d 2747 |
. . . . . 6
β’ (π = suc βͺ (π΄
βͺ π΅) β ((π΄ β© π) = (π΅ β© π) β (π΄ β© suc βͺ
(π΄ βͺ π΅)) = (π΅ β© suc βͺ
(π΄ βͺ π΅)))) |
48 | 46, 47 | imbi12d 343 |
. . . . 5
β’ (π = suc βͺ (π΄
βͺ π΅) β (((πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)) β (π΄ β© π) = (π΅ β© π)) β ((πΉβ(π΄ β© suc βͺ
(π΄ βͺ π΅))) = (πΉβ(π΅ β© suc βͺ
(π΄ βͺ π΅))) β (π΄ β© suc βͺ
(π΄ βͺ π΅)) = (π΅ β© suc βͺ
(π΄ βͺ π΅))))) |
49 | 48 | imbi2d 339 |
. . . 4
β’ (π = suc βͺ (π΄
βͺ π΅) β (((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β ((πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)) β (π΄ β© π) = (π΅ β© π))) β ((π΄ β (π« Ο β© Fin) β§
π΅ β (π« Ο
β© Fin)) β ((πΉβ(π΄ β© suc βͺ
(π΄ βͺ π΅))) = (πΉβ(π΅ β© suc βͺ
(π΄ βͺ π΅))) β (π΄ β© suc βͺ
(π΄ βͺ π΅)) = (π΅ β© suc βͺ
(π΄ βͺ π΅)))))) |
50 | | in0 4392 |
. . . . . 6
β’ (π΄ β© β
) =
β
|
51 | | in0 4392 |
. . . . . 6
β’ (π΅ β© β
) =
β
|
52 | 50, 51 | eqtr4i 2762 |
. . . . 5
β’ (π΄ β© β
) = (π΅ β© β
) |
53 | 52 | 2a1i 12 |
. . . 4
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β ((πΉβ(π΄ β© β
)) = (πΉβ(π΅ β© β
)) β (π΄ β© β
) = (π΅ β© β
))) |
54 | | simp13 1204 |
. . . . . . . . . . . . 13
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β§ π β π΄ β§ π β π΅) β (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) |
55 | | 3simpa 1147 |
. . . . . . . . . . . . . 14
β’ ((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β (π β Ο β§ (π΄ β (π« Ο β© Fin) β§
π΅ β (π« Ο
β© Fin)))) |
56 | | ackbij1lem2 10219 |
. . . . . . . . . . . . . . . . 17
β’ (π β π΄ β (π΄ β© suc π) = ({π} βͺ (π΄ β© π))) |
57 | 56 | fveq2d 6896 |
. . . . . . . . . . . . . . . 16
β’ (π β π΄ β (πΉβ(π΄ β© suc π)) = (πΉβ({π} βͺ (π΄ β© π)))) |
58 | 57 | 3ad2ant2 1133 |
. . . . . . . . . . . . . . 15
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin))) β§ π β π΄ β§ π β π΅) β (πΉβ(π΄ β© suc π)) = (πΉβ({π} βͺ (π΄ β© π)))) |
59 | | ackbij1lem4 10221 |
. . . . . . . . . . . . . . . . . 18
β’ (π β Ο β {π} β (π« Ο
β© Fin)) |
60 | 59 | adantr 480 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin))) β {π} β (π« Ο β©
Fin)) |
61 | | simprl 768 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin))) β π΄ β (π« Ο β©
Fin)) |
62 | | inss1 4229 |
. . . . . . . . . . . . . . . . . 18
β’ (π΄ β© π) β π΄ |
63 | | ackbij.f |
. . . . . . . . . . . . . . . . . . 19
β’ πΉ = (π₯ β (π« Ο β© Fin) β¦
(cardββͺ π¦ β π₯ ({π¦} Γ π« π¦))) |
64 | 63 | ackbij1lem11 10228 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β (π« Ο β©
Fin) β§ (π΄ β© π) β π΄) β (π΄ β© π) β (π« Ο β©
Fin)) |
65 | 61, 62, 64 | sylancl 585 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin))) β (π΄ β© π) β (π« Ο β©
Fin)) |
66 | | incom 4202 |
. . . . . . . . . . . . . . . . . 18
β’ ({π} β© (π΄ β© π)) = ((π΄ β© π) β© {π}) |
67 | | inss2 4230 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΄ β© π) β π |
68 | | nnord 7866 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β Ο β Ord π) |
69 | | orddisj 6403 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (Ord
π β (π β© {π}) = β
) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β Ο β (π β© {π}) = β
) |
71 | 70 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin))) β (π β© {π}) = β
) |
72 | | ssdisj 4460 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π΄ β© π) β π β§ (π β© {π}) = β
) β ((π΄ β© π) β© {π}) = β
) |
73 | 67, 71, 72 | sylancr 586 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin))) β ((π΄ β© π) β© {π}) = β
) |
74 | 66, 73 | eqtrid 2783 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin))) β ({π} β© (π΄ β© π)) = β
) |
75 | 63 | ackbij1lem9 10226 |
. . . . . . . . . . . . . . . . 17
β’ (({π} β (π« Ο
β© Fin) β§ (π΄ β©
π) β (π«
Ο β© Fin) β§ ({π} β© (π΄ β© π)) = β
) β (πΉβ({π} βͺ (π΄ β© π))) = ((πΉβ{π}) +o (πΉβ(π΄ β© π)))) |
76 | 60, 65, 74, 75 | syl3anc 1370 |
. . . . . . . . . . . . . . . 16
β’ ((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin))) β (πΉβ({π} βͺ (π΄ β© π))) = ((πΉβ{π}) +o (πΉβ(π΄ β© π)))) |
77 | 76 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . 15
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin))) β§ π β π΄ β§ π β π΅) β (πΉβ({π} βͺ (π΄ β© π))) = ((πΉβ{π}) +o (πΉβ(π΄ β© π)))) |
78 | 58, 77 | eqtrd 2771 |
. . . . . . . . . . . . . 14
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin))) β§ π β π΄ β§ π β π΅) β (πΉβ(π΄ β© suc π)) = ((πΉβ{π}) +o (πΉβ(π΄ β© π)))) |
79 | 55, 78 | syl3an1 1162 |
. . . . . . . . . . . . 13
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β§ π β π΄ β§ π β π΅) β (πΉβ(π΄ β© suc π)) = ((πΉβ{π}) +o (πΉβ(π΄ β© π)))) |
80 | | ackbij1lem2 10219 |
. . . . . . . . . . . . . . . . 17
β’ (π β π΅ β (π΅ β© suc π) = ({π} βͺ (π΅ β© π))) |
81 | 80 | fveq2d 6896 |
. . . . . . . . . . . . . . . 16
β’ (π β π΅ β (πΉβ(π΅ β© suc π)) = (πΉβ({π} βͺ (π΅ β© π)))) |
82 | 81 | 3ad2ant3 1134 |
. . . . . . . . . . . . . . 15
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin))) β§ π β π΄ β§ π β π΅) β (πΉβ(π΅ β© suc π)) = (πΉβ({π} βͺ (π΅ β© π)))) |
83 | | simprr 770 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin))) β π΅ β (π« Ο β©
Fin)) |
84 | | inss1 4229 |
. . . . . . . . . . . . . . . . . 18
β’ (π΅ β© π) β π΅ |
85 | 63 | ackbij1lem11 10228 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΅ β (π« Ο β©
Fin) β§ (π΅ β© π) β π΅) β (π΅ β© π) β (π« Ο β©
Fin)) |
86 | 83, 84, 85 | sylancl 585 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin))) β (π΅ β© π) β (π« Ο β©
Fin)) |
87 | | incom 4202 |
. . . . . . . . . . . . . . . . . 18
β’ ({π} β© (π΅ β© π)) = ((π΅ β© π) β© {π}) |
88 | | inss2 4230 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΅ β© π) β π |
89 | | ssdisj 4460 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π΅ β© π) β π β§ (π β© {π}) = β
) β ((π΅ β© π) β© {π}) = β
) |
90 | 88, 71, 89 | sylancr 586 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin))) β ((π΅ β© π) β© {π}) = β
) |
91 | 87, 90 | eqtrid 2783 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin))) β ({π} β© (π΅ β© π)) = β
) |
92 | 63 | ackbij1lem9 10226 |
. . . . . . . . . . . . . . . . 17
β’ (({π} β (π« Ο
β© Fin) β§ (π΅ β©
π) β (π«
Ο β© Fin) β§ ({π} β© (π΅ β© π)) = β
) β (πΉβ({π} βͺ (π΅ β© π))) = ((πΉβ{π}) +o (πΉβ(π΅ β© π)))) |
93 | 60, 86, 91, 92 | syl3anc 1370 |
. . . . . . . . . . . . . . . 16
β’ ((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin))) β (πΉβ({π} βͺ (π΅ β© π))) = ((πΉβ{π}) +o (πΉβ(π΅ β© π)))) |
94 | 93 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . 15
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin))) β§ π β π΄ β§ π β π΅) β (πΉβ({π} βͺ (π΅ β© π))) = ((πΉβ{π}) +o (πΉβ(π΅ β© π)))) |
95 | 82, 94 | eqtrd 2771 |
. . . . . . . . . . . . . 14
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin))) β§ π β π΄ β§ π β π΅) β (πΉβ(π΅ β© suc π)) = ((πΉβ{π}) +o (πΉβ(π΅ β© π)))) |
96 | 55, 95 | syl3an1 1162 |
. . . . . . . . . . . . 13
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β§ π β π΄ β§ π β π΅) β (πΉβ(π΅ β© suc π)) = ((πΉβ{π}) +o (πΉβ(π΅ β© π)))) |
97 | 54, 79, 96 | 3eqtr3d 2779 |
. . . . . . . . . . . 12
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β§ π β π΄ β§ π β π΅) β ((πΉβ{π}) +o (πΉβ(π΄ β© π))) = ((πΉβ{π}) +o (πΉβ(π΅ β© π)))) |
98 | 63 | ackbij1lem10 10227 |
. . . . . . . . . . . . . . . . 17
β’ πΉ:(π« Ο β©
Fin)βΆΟ |
99 | 98 | ffvelcdmi 7086 |
. . . . . . . . . . . . . . . 16
β’ ({π} β (π« Ο
β© Fin) β (πΉβ{π}) β Ο) |
100 | 60, 99 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin))) β (πΉβ{π}) β Ο) |
101 | 98 | ffvelcdmi 7086 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β© π) β (π« Ο β© Fin) β
(πΉβ(π΄ β© π)) β Ο) |
102 | 65, 101 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin))) β (πΉβ(π΄ β© π)) β Ο) |
103 | 98 | ffvelcdmi 7086 |
. . . . . . . . . . . . . . . 16
β’ ((π΅ β© π) β (π« Ο β© Fin) β
(πΉβ(π΅ β© π)) β Ο) |
104 | 86, 103 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin))) β (πΉβ(π΅ β© π)) β Ο) |
105 | | nnacan 8631 |
. . . . . . . . . . . . . . 15
β’ (((πΉβ{π}) β Ο β§ (πΉβ(π΄ β© π)) β Ο β§ (πΉβ(π΅ β© π)) β Ο) β (((πΉβ{π}) +o (πΉβ(π΄ β© π))) = ((πΉβ{π}) +o (πΉβ(π΅ β© π))) β (πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)))) |
106 | 100, 102,
104, 105 | syl3anc 1370 |
. . . . . . . . . . . . . 14
β’ ((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin))) β (((πΉβ{π}) +o (πΉβ(π΄ β© π))) = ((πΉβ{π}) +o (πΉβ(π΅ β© π))) β (πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)))) |
107 | 106 | 3adant3 1131 |
. . . . . . . . . . . . 13
β’ ((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β (((πΉβ{π}) +o (πΉβ(π΄ β© π))) = ((πΉβ{π}) +o (πΉβ(π΅ β© π))) β (πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)))) |
108 | 107 | 3ad2ant1 1132 |
. . . . . . . . . . . 12
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β§ π β π΄ β§ π β π΅) β (((πΉβ{π}) +o (πΉβ(π΄ β© π))) = ((πΉβ{π}) +o (πΉβ(π΅ β© π))) β (πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)))) |
109 | 97, 108 | mpbid 231 |
. . . . . . . . . . 11
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β§ π β π΄ β§ π β π΅) β (πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π))) |
110 | | uneq2 4158 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β© π) = (π΅ β© π) β ({π} βͺ (π΄ β© π)) = ({π} βͺ (π΅ β© π))) |
111 | 110 | adantl 481 |
. . . . . . . . . . . . . 14
β’ (((π β π΄ β§ π β π΅) β§ (π΄ β© π) = (π΅ β© π)) β ({π} βͺ (π΄ β© π)) = ({π} βͺ (π΅ β© π))) |
112 | 56 | ad2antrr 723 |
. . . . . . . . . . . . . 14
β’ (((π β π΄ β§ π β π΅) β§ (π΄ β© π) = (π΅ β© π)) β (π΄ β© suc π) = ({π} βͺ (π΄ β© π))) |
113 | 80 | ad2antlr 724 |
. . . . . . . . . . . . . 14
β’ (((π β π΄ β§ π β π΅) β§ (π΄ β© π) = (π΅ β© π)) β (π΅ β© suc π) = ({π} βͺ (π΅ β© π))) |
114 | 111, 112,
113 | 3eqtr4d 2781 |
. . . . . . . . . . . . 13
β’ (((π β π΄ β§ π β π΅) β§ (π΄ β© π) = (π΅ β© π)) β (π΄ β© suc π) = (π΅ β© suc π)) |
115 | 114 | ex 412 |
. . . . . . . . . . . 12
β’ ((π β π΄ β§ π β π΅) β ((π΄ β© π) = (π΅ β© π) β (π΄ β© suc π) = (π΅ β© suc π))) |
116 | 115 | 3adant1 1129 |
. . . . . . . . . . 11
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β§ π β π΄ β§ π β π΅) β ((π΄ β© π) = (π΅ β© π) β (π΄ β© suc π) = (π΅ β© suc π))) |
117 | 109, 116 | embantd 59 |
. . . . . . . . . 10
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β§ π β π΄ β§ π β π΅) β (((πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)) β (π΄ β© π) = (π΅ β© π)) β (π΄ β© suc π) = (π΅ β© suc π))) |
118 | 117 | 3exp 1118 |
. . . . . . . . 9
β’ ((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β (π β π΄ β (π β π΅ β (((πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)) β (π΄ β© π) = (π΅ β© π)) β (π΄ β© suc π) = (π΅ β© suc π))))) |
119 | | simp13 1204 |
. . . . . . . . . . . 12
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β§ Β¬ π β π΄ β§ π β π΅) β (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) |
120 | 119 | eqcomd 2737 |
. . . . . . . . . . 11
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β§ Β¬ π β π΄ β§ π β π΅) β (πΉβ(π΅ β© suc π)) = (πΉβ(π΄ β© suc π))) |
121 | | simp12r 1286 |
. . . . . . . . . . . 12
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β§ Β¬ π β π΄ β§ π β π΅) β π΅ β (π« Ο β©
Fin)) |
122 | | simp12l 1285 |
. . . . . . . . . . . 12
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β§ Β¬ π β π΄ β§ π β π΅) β π΄ β (π« Ο β©
Fin)) |
123 | | simp11 1202 |
. . . . . . . . . . . 12
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β§ Β¬ π β π΄ β§ π β π΅) β π β Ο) |
124 | | simp3 1137 |
. . . . . . . . . . . 12
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β§ Β¬ π β π΄ β§ π β π΅) β π β π΅) |
125 | | simp2 1136 |
. . . . . . . . . . . 12
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β§ Β¬ π β π΄ β§ π β π΅) β Β¬ π β π΄) |
126 | 63 | ackbij1lem15 10232 |
. . . . . . . . . . . 12
β’ (((π΅ β (π« Ο β©
Fin) β§ π΄ β
(π« Ο β© Fin)) β§ (π β Ο β§ π β π΅ β§ Β¬ π β π΄)) β Β¬ (πΉβ(π΅ β© suc π)) = (πΉβ(π΄ β© suc π))) |
127 | 121, 122,
123, 124, 125, 126 | syl23anc 1376 |
. . . . . . . . . . 11
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β§ Β¬ π β π΄ β§ π β π΅) β Β¬ (πΉβ(π΅ β© suc π)) = (πΉβ(π΄ β© suc π))) |
128 | 120, 127 | pm2.21dd 194 |
. . . . . . . . . 10
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β§ Β¬ π β π΄ β§ π β π΅) β (((πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)) β (π΄ β© π) = (π΅ β© π)) β (π΄ β© suc π) = (π΅ β© suc π))) |
129 | 128 | 3exp 1118 |
. . . . . . . . 9
β’ ((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β (Β¬ π β π΄ β (π β π΅ β (((πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)) β (π΄ β© π) = (π΅ β© π)) β (π΄ β© suc π) = (π΅ β© suc π))))) |
130 | 118, 129 | pm2.61d 179 |
. . . . . . . 8
β’ ((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β (π β π΅ β (((πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)) β (π΄ β© π) = (π΅ β© π)) β (π΄ β© suc π) = (π΅ β© suc π)))) |
131 | | simp13 1204 |
. . . . . . . . . . 11
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β§ π β π΄ β§ Β¬ π β π΅) β (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) |
132 | | simp12l 1285 |
. . . . . . . . . . . 12
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β§ π β π΄ β§ Β¬ π β π΅) β π΄ β (π« Ο β©
Fin)) |
133 | | simp12r 1286 |
. . . . . . . . . . . 12
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β§ π β π΄ β§ Β¬ π β π΅) β π΅ β (π« Ο β©
Fin)) |
134 | | simp11 1202 |
. . . . . . . . . . . 12
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β§ π β π΄ β§ Β¬ π β π΅) β π β Ο) |
135 | | simp2 1136 |
. . . . . . . . . . . 12
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β§ π β π΄ β§ Β¬ π β π΅) β π β π΄) |
136 | | simp3 1137 |
. . . . . . . . . . . 12
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β§ π β π΄ β§ Β¬ π β π΅) β Β¬ π β π΅) |
137 | 63 | ackbij1lem15 10232 |
. . . . . . . . . . . 12
β’ (((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (π β Ο β§ π β π΄ β§ Β¬ π β π΅)) β Β¬ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) |
138 | 132, 133,
134, 135, 136, 137 | syl23anc 1376 |
. . . . . . . . . . 11
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β§ π β π΄ β§ Β¬ π β π΅) β Β¬ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) |
139 | 131, 138 | pm2.21dd 194 |
. . . . . . . . . 10
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β§ π β π΄ β§ Β¬ π β π΅) β (((πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)) β (π΄ β© π) = (π΅ β© π)) β (π΄ β© suc π) = (π΅ β© suc π))) |
140 | 139 | 3exp 1118 |
. . . . . . . . 9
β’ ((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β (π β π΄ β (Β¬ π β π΅ β (((πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)) β (π΄ β© π) = (π΅ β© π)) β (π΄ β© suc π) = (π΅ β© suc π))))) |
141 | | simp13 1204 |
. . . . . . . . . . . 12
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β§ Β¬ π β π΄ β§ Β¬ π β π΅) β (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) |
142 | | ackbij1lem1 10218 |
. . . . . . . . . . . . . . . . 17
β’ (Β¬
π β π΄ β (π΄ β© suc π) = (π΄ β© π)) |
143 | 142 | adantr 480 |
. . . . . . . . . . . . . . . 16
β’ ((Β¬
π β π΄ β§ Β¬ π β π΅) β (π΄ β© suc π) = (π΄ β© π)) |
144 | 143 | fveq2d 6896 |
. . . . . . . . . . . . . . 15
β’ ((Β¬
π β π΄ β§ Β¬ π β π΅) β (πΉβ(π΄ β© suc π)) = (πΉβ(π΄ β© π))) |
145 | | ackbij1lem1 10218 |
. . . . . . . . . . . . . . . . 17
β’ (Β¬
π β π΅ β (π΅ β© suc π) = (π΅ β© π)) |
146 | 145 | adantl 481 |
. . . . . . . . . . . . . . . 16
β’ ((Β¬
π β π΄ β§ Β¬ π β π΅) β (π΅ β© suc π) = (π΅ β© π)) |
147 | 146 | fveq2d 6896 |
. . . . . . . . . . . . . . 15
β’ ((Β¬
π β π΄ β§ Β¬ π β π΅) β (πΉβ(π΅ β© suc π)) = (πΉβ(π΅ β© π))) |
148 | 144, 147 | eqeq12d 2747 |
. . . . . . . . . . . . . 14
β’ ((Β¬
π β π΄ β§ Β¬ π β π΅) β ((πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π)) β (πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)))) |
149 | 148 | biimpd 228 |
. . . . . . . . . . . . 13
β’ ((Β¬
π β π΄ β§ Β¬ π β π΅) β ((πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π)) β (πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)))) |
150 | 149 | 3adant1 1129 |
. . . . . . . . . . . 12
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β§ Β¬ π β π΄ β§ Β¬ π β π΅) β ((πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π)) β (πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)))) |
151 | 141, 150 | mpd 15 |
. . . . . . . . . . 11
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β§ Β¬ π β π΄ β§ Β¬ π β π΅) β (πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π))) |
152 | 143, 146 | eqeq12d 2747 |
. . . . . . . . . . . . 13
β’ ((Β¬
π β π΄ β§ Β¬ π β π΅) β ((π΄ β© suc π) = (π΅ β© suc π) β (π΄ β© π) = (π΅ β© π))) |
153 | 152 | biimprd 247 |
. . . . . . . . . . . 12
β’ ((Β¬
π β π΄ β§ Β¬ π β π΅) β ((π΄ β© π) = (π΅ β© π) β (π΄ β© suc π) = (π΅ β© suc π))) |
154 | 153 | 3adant1 1129 |
. . . . . . . . . . 11
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β§ Β¬ π β π΄ β§ Β¬ π β π΅) β ((π΄ β© π) = (π΅ β© π) β (π΄ β© suc π) = (π΅ β© suc π))) |
155 | 151, 154 | embantd 59 |
. . . . . . . . . 10
β’ (((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β§ Β¬ π β π΄ β§ Β¬ π β π΅) β (((πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)) β (π΄ β© π) = (π΅ β© π)) β (π΄ β© suc π) = (π΅ β© suc π))) |
156 | 155 | 3exp 1118 |
. . . . . . . . 9
β’ ((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β (Β¬ π β π΄ β (Β¬ π β π΅ β (((πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)) β (π΄ β© π) = (π΅ β© π)) β (π΄ β© suc π) = (π΅ β© suc π))))) |
157 | 140, 156 | pm2.61d 179 |
. . . . . . . 8
β’ ((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β (Β¬ π β π΅ β (((πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)) β (π΄ β© π) = (π΅ β© π)) β (π΄ β© suc π) = (π΅ β© suc π)))) |
158 | 130, 157 | pm2.61d 179 |
. . . . . . 7
β’ ((π β Ο β§ (π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) β (((πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)) β (π΄ β© π) = (π΅ β© π)) β (π΄ β© suc π) = (π΅ β© suc π))) |
159 | 158 | 3exp 1118 |
. . . . . 6
β’ (π β Ο β ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β ((πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π)) β (((πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)) β (π΄ β© π) = (π΅ β© π)) β (π΄ β© suc π) = (π΅ β© suc π))))) |
160 | 159 | com34 91 |
. . . . 5
β’ (π β Ο β ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β (((πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)) β (π΄ β© π) = (π΅ β© π)) β ((πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π)) β (π΄ β© suc π) = (π΅ β© suc π))))) |
161 | 160 | a2d 29 |
. . . 4
β’ (π β Ο β (((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β ((πΉβ(π΄ β© π)) = (πΉβ(π΅ β© π)) β (π΄ β© π) = (π΅ β© π))) β ((π΄ β (π« Ο β© Fin) β§
π΅ β (π« Ο
β© Fin)) β ((πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π)) β (π΄ β© suc π) = (π΅ β© suc π))))) |
162 | 25, 33, 41, 49, 53, 161 | finds 7892 |
. . 3
β’ (suc
βͺ (π΄ βͺ π΅) β Ο β ((π΄ β (π« Ο β© Fin) β§
π΅ β (π« Ο
β© Fin)) β ((πΉβ(π΄ β© suc βͺ
(π΄ βͺ π΅))) = (πΉβ(π΅ β© suc βͺ
(π΄ βͺ π΅))) β (π΄ β© suc βͺ
(π΄ βͺ π΅)) = (π΅ β© suc βͺ
(π΄ βͺ π΅))))) |
163 | 17, 162 | mpcom 38 |
. 2
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β ((πΉβ(π΄ β© suc βͺ
(π΄ βͺ π΅))) = (πΉβ(π΅ β© suc βͺ
(π΄ βͺ π΅))) β (π΄ β© suc βͺ
(π΄ βͺ π΅)) = (π΅ β© suc βͺ
(π΄ βͺ π΅)))) |
164 | | omsson 7862 |
. . . . . . . 8
β’ Ο
β On |
165 | 8, 164 | sstrdi 3995 |
. . . . . . 7
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β (π΄ βͺ π΅) β On) |
166 | | onsucuni 7819 |
. . . . . . 7
β’ ((π΄ βͺ π΅) β On β (π΄ βͺ π΅) β suc βͺ
(π΄ βͺ π΅)) |
167 | 165, 166 | syl 17 |
. . . . . 6
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β (π΄ βͺ π΅) β suc βͺ
(π΄ βͺ π΅)) |
168 | 167 | unssad 4188 |
. . . . 5
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β π΄ β suc βͺ
(π΄ βͺ π΅)) |
169 | | df-ss 3966 |
. . . . 5
β’ (π΄ β suc βͺ (π΄
βͺ π΅) β (π΄ β© suc βͺ (π΄
βͺ π΅)) = π΄) |
170 | 168, 169 | sylib 217 |
. . . 4
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β (π΄ β© suc βͺ
(π΄ βͺ π΅)) = π΄) |
171 | 170 | fveq2d 6896 |
. . 3
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β (πΉβ(π΄ β© suc βͺ
(π΄ βͺ π΅))) = (πΉβπ΄)) |
172 | 167 | unssbd 4189 |
. . . . 5
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β π΅ β suc βͺ
(π΄ βͺ π΅)) |
173 | | df-ss 3966 |
. . . . 5
β’ (π΅ β suc βͺ (π΄
βͺ π΅) β (π΅ β© suc βͺ (π΄
βͺ π΅)) = π΅) |
174 | 172, 173 | sylib 217 |
. . . 4
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β (π΅ β© suc βͺ
(π΄ βͺ π΅)) = π΅) |
175 | 174 | fveq2d 6896 |
. . 3
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β (πΉβ(π΅ β© suc βͺ
(π΄ βͺ π΅))) = (πΉβπ΅)) |
176 | 171, 175 | eqeq12d 2747 |
. 2
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β ((πΉβ(π΄ β© suc βͺ
(π΄ βͺ π΅))) = (πΉβ(π΅ β© suc βͺ
(π΄ βͺ π΅))) β (πΉβπ΄) = (πΉβπ΅))) |
177 | 170, 174 | eqeq12d 2747 |
. 2
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β ((π΄ β© suc βͺ
(π΄ βͺ π΅)) = (π΅ β© suc βͺ
(π΄ βͺ π΅)) β π΄ = π΅)) |
178 | 163, 176,
177 | 3imtr3d 292 |
1
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β ((πΉβπ΄) = (πΉβπ΅) β π΄ = π΅)) |