Step | Hyp | Ref
| Expression |
1 | | simpr1 1195 |
. . . . . . 7
β’ (((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (π β Ο β§ π β π΄ β§ Β¬ π β π΅)) β π β Ο) |
2 | | ackbij1lem3 10166 |
. . . . . . 7
β’ (π β Ο β π β (π« Ο β©
Fin)) |
3 | 1, 2 | syl 17 |
. . . . . 6
β’ (((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (π β Ο β§ π β π΄ β§ Β¬ π β π΅)) β π β (π« Ο β©
Fin)) |
4 | | simpr3 1197 |
. . . . . . . 8
β’ (((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (π β Ο β§ π β π΄ β§ Β¬ π β π΅)) β Β¬ π β π΅) |
5 | | ackbij1lem1 10164 |
. . . . . . . 8
β’ (Β¬
π β π΅ β (π΅ β© suc π) = (π΅ β© π)) |
6 | 4, 5 | syl 17 |
. . . . . . 7
β’ (((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (π β Ο β§ π β π΄ β§ Β¬ π β π΅)) β (π΅ β© suc π) = (π΅ β© π)) |
7 | | inss2 4193 |
. . . . . . 7
β’ (π΅ β© π) β π |
8 | 6, 7 | eqsstrdi 4002 |
. . . . . 6
β’ (((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (π β Ο β§ π β π΄ β§ Β¬ π β π΅)) β (π΅ β© suc π) β π) |
9 | | ackbij.f |
. . . . . . 7
β’ πΉ = (π₯ β (π« Ο β© Fin) β¦
(cardββͺ π¦ β π₯ ({π¦} Γ π« π¦))) |
10 | 9 | ackbij1lem12 10175 |
. . . . . 6
β’ ((π β (π« Ο β©
Fin) β§ (π΅ β© suc
π) β π) β (πΉβ(π΅ β© suc π)) β (πΉβπ)) |
11 | 3, 8, 10 | syl2anc 585 |
. . . . 5
β’ (((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (π β Ο β§ π β π΄ β§ Β¬ π β π΅)) β (πΉβ(π΅ β© suc π)) β (πΉβπ)) |
12 | 9 | ackbij1lem10 10173 |
. . . . . . . . 9
β’ πΉ:(π« Ο β©
Fin)βΆΟ |
13 | 12 | ffvelcdmi 7038 |
. . . . . . . 8
β’ (π β (π« Ο β©
Fin) β (πΉβπ) β
Ο) |
14 | | nnon 7812 |
. . . . . . . 8
β’ ((πΉβπ) β Ο β (πΉβπ) β On) |
15 | | onpsssuc 7758 |
. . . . . . . 8
β’ ((πΉβπ) β On β (πΉβπ) β suc (πΉβπ)) |
16 | 3, 13, 14, 15 | 4syl 19 |
. . . . . . 7
β’ (((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (π β Ο β§ π β π΄ β§ Β¬ π β π΅)) β (πΉβπ) β suc (πΉβπ)) |
17 | 9 | ackbij1lem14 10177 |
. . . . . . . . 9
β’ (π β Ο β (πΉβ{π}) = suc (πΉβπ)) |
18 | 1, 17 | syl 17 |
. . . . . . . 8
β’ (((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (π β Ο β§ π β π΄ β§ Β¬ π β π΅)) β (πΉβ{π}) = suc (πΉβπ)) |
19 | 18 | psseq2d 4057 |
. . . . . . 7
β’ (((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (π β Ο β§ π β π΄ β§ Β¬ π β π΅)) β ((πΉβπ) β (πΉβ{π}) β (πΉβπ) β suc (πΉβπ))) |
20 | 16, 19 | mpbird 257 |
. . . . . 6
β’ (((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (π β Ο β§ π β π΄ β§ Β¬ π β π΅)) β (πΉβπ) β (πΉβ{π})) |
21 | | simpll 766 |
. . . . . . . 8
β’ (((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (π β Ο β§ π β π΄ β§ Β¬ π β π΅)) β π΄ β (π« Ο β©
Fin)) |
22 | | inss1 4192 |
. . . . . . . 8
β’ (π΄ β© suc π) β π΄ |
23 | 9 | ackbij1lem11 10174 |
. . . . . . . 8
β’ ((π΄ β (π« Ο β©
Fin) β§ (π΄ β© suc
π) β π΄) β (π΄ β© suc π) β (π« Ο β©
Fin)) |
24 | 21, 22, 23 | sylancl 587 |
. . . . . . 7
β’ (((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (π β Ο β§ π β π΄ β§ Β¬ π β π΅)) β (π΄ β© suc π) β (π« Ο β©
Fin)) |
25 | | ssun1 4136 |
. . . . . . . 8
β’ {π} β ({π} βͺ (π΄ β© π)) |
26 | | simpr2 1196 |
. . . . . . . . 9
β’ (((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (π β Ο β§ π β π΄ β§ Β¬ π β π΅)) β π β π΄) |
27 | | ackbij1lem2 10165 |
. . . . . . . . 9
β’ (π β π΄ β (π΄ β© suc π) = ({π} βͺ (π΄ β© π))) |
28 | 26, 27 | syl 17 |
. . . . . . . 8
β’ (((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (π β Ο β§ π β π΄ β§ Β¬ π β π΅)) β (π΄ β© suc π) = ({π} βͺ (π΄ β© π))) |
29 | 25, 28 | sseqtrrid 4001 |
. . . . . . 7
β’ (((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (π β Ο β§ π β π΄ β§ Β¬ π β π΅)) β {π} β (π΄ β© suc π)) |
30 | 9 | ackbij1lem12 10175 |
. . . . . . 7
β’ (((π΄ β© suc π) β (π« Ο β© Fin) β§
{π} β (π΄ β© suc π)) β (πΉβ{π}) β (πΉβ(π΄ β© suc π))) |
31 | 24, 29, 30 | syl2anc 585 |
. . . . . 6
β’ (((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (π β Ο β§ π β π΄ β§ Β¬ π β π΅)) β (πΉβ{π}) β (πΉβ(π΄ β© suc π))) |
32 | 20, 31 | psssstrd 4073 |
. . . . 5
β’ (((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (π β Ο β§ π β π΄ β§ Β¬ π β π΅)) β (πΉβπ) β (πΉβ(π΄ β© suc π))) |
33 | 11, 32 | sspsstrd 4072 |
. . . 4
β’ (((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (π β Ο β§ π β π΄ β§ Β¬ π β π΅)) β (πΉβ(π΅ β© suc π)) β (πΉβ(π΄ β© suc π))) |
34 | 33 | pssned 4062 |
. . 3
β’ (((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (π β Ο β§ π β π΄ β§ Β¬ π β π΅)) β (πΉβ(π΅ β© suc π)) β (πΉβ(π΄ β© suc π))) |
35 | 34 | necomd 2996 |
. 2
β’ (((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (π β Ο β§ π β π΄ β§ Β¬ π β π΅)) β (πΉβ(π΄ β© suc π)) β (πΉβ(π΅ β© suc π))) |
36 | 35 | neneqd 2945 |
1
β’ (((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β§ (π β Ο β§ π β π΄ β§ Β¬ π β π΅)) β Β¬ (πΉβ(π΄ β© suc π)) = (πΉβ(π΅ β© suc π))) |