Step | Hyp | Ref
| Expression |
1 | | ackbij.f |
. . . . . 6
β’ πΉ = (π₯ β (π« Ο β© Fin) β¦
(cardββͺ π¦ β π₯ ({π¦} Γ π« π¦))) |
2 | 1 | ackbij1lem17 10233 |
. . . . 5
β’ πΉ:(π« Ο β©
Fin)β1-1βΟ |
3 | | ackbij2lem1 10216 |
. . . . 5
β’ (π΄ β Ο β π«
π΄ β (π«
Ο β© Fin)) |
4 | | pwexg 5376 |
. . . . 5
β’ (π΄ β Ο β π«
π΄ β
V) |
5 | | f1imaeng 9012 |
. . . . 5
β’ ((πΉ:(π« Ο β©
Fin)β1-1βΟ β§
π« π΄ β
(π« Ο β© Fin) β§ π« π΄ β V) β (πΉ β π« π΄) β π« π΄) |
6 | 2, 3, 4, 5 | mp3an2i 1466 |
. . . 4
β’ (π΄ β Ο β (πΉ β π« π΄) β π« π΄) |
7 | | nnfi 9169 |
. . . . . 6
β’ (π΄ β Ο β π΄ β Fin) |
8 | | pwfi 9180 |
. . . . . 6
β’ (π΄ β Fin β π«
π΄ β
Fin) |
9 | 7, 8 | sylib 217 |
. . . . 5
β’ (π΄ β Ο β π«
π΄ β
Fin) |
10 | | ficardid 9959 |
. . . . 5
β’
(π« π΄ β
Fin β (cardβπ« π΄) β π« π΄) |
11 | | ensym 9001 |
. . . . 5
β’
((cardβπ« π΄) β π« π΄ β π« π΄ β (cardβπ« π΄)) |
12 | 9, 10, 11 | 3syl 18 |
. . . 4
β’ (π΄ β Ο β π«
π΄ β
(cardβπ« π΄)) |
13 | | entr 9004 |
. . . 4
β’ (((πΉ β π« π΄) β π« π΄ β§ π« π΄ β (cardβπ«
π΄)) β (πΉ β π« π΄) β (cardβπ«
π΄)) |
14 | 6, 12, 13 | syl2anc 584 |
. . 3
β’ (π΄ β Ο β (πΉ β π« π΄) β (cardβπ«
π΄)) |
15 | | onfin2 9233 |
. . . . . . 7
β’ Ο =
(On β© Fin) |
16 | | inss2 4229 |
. . . . . . 7
β’ (On β©
Fin) β Fin |
17 | 15, 16 | eqsstri 4016 |
. . . . . 6
β’ Ο
β Fin |
18 | | ficardom 9958 |
. . . . . . 7
β’
(π« π΄ β
Fin β (cardβπ« π΄) β Ο) |
19 | 9, 18 | syl 17 |
. . . . . 6
β’ (π΄ β Ο β
(cardβπ« π΄)
β Ο) |
20 | 17, 19 | sselid 3980 |
. . . . 5
β’ (π΄ β Ο β
(cardβπ« π΄)
β Fin) |
21 | | php3 9214 |
. . . . . 6
β’
(((cardβπ« π΄) β Fin β§ (πΉ β π« π΄) β (cardβπ« π΄)) β (πΉ β π« π΄) βΊ (cardβπ« π΄)) |
22 | 21 | ex 413 |
. . . . 5
β’
((cardβπ« π΄) β Fin β ((πΉ β π« π΄) β (cardβπ« π΄) β (πΉ β π« π΄) βΊ (cardβπ« π΄))) |
23 | 20, 22 | syl 17 |
. . . 4
β’ (π΄ β Ο β ((πΉ β π« π΄) β (cardβπ«
π΄) β (πΉ β π« π΄) βΊ (cardβπ«
π΄))) |
24 | | sdomnen 8979 |
. . . 4
β’ ((πΉ β π« π΄) βΊ (cardβπ«
π΄) β Β¬ (πΉ β π« π΄) β (cardβπ«
π΄)) |
25 | 23, 24 | syl6 35 |
. . 3
β’ (π΄ β Ο β ((πΉ β π« π΄) β (cardβπ«
π΄) β Β¬ (πΉ β π« π΄) β (cardβπ«
π΄))) |
26 | 14, 25 | mt2d 136 |
. 2
β’ (π΄ β Ο β Β¬
(πΉ β π« π΄) β (cardβπ«
π΄)) |
27 | | fvex 6904 |
. . . . . 6
β’ (πΉβπ) β V |
28 | | ackbij1lem3 10219 |
. . . . . . . . 9
β’ (π΄ β Ο β π΄ β (π« Ο β©
Fin)) |
29 | | elpwi 4609 |
. . . . . . . . 9
β’ (π β π« π΄ β π β π΄) |
30 | 1 | ackbij1lem12 10228 |
. . . . . . . . 9
β’ ((π΄ β (π« Ο β©
Fin) β§ π β π΄) β (πΉβπ) β (πΉβπ΄)) |
31 | 28, 29, 30 | syl2an 596 |
. . . . . . . 8
β’ ((π΄ β Ο β§ π β π« π΄) β (πΉβπ) β (πΉβπ΄)) |
32 | 1 | ackbij1lem10 10226 |
. . . . . . . . . . 11
β’ πΉ:(π« Ο β©
Fin)βΆΟ |
33 | | peano1 7881 |
. . . . . . . . . . 11
β’ β
β Ο |
34 | 32, 33 | f0cli 7099 |
. . . . . . . . . 10
β’ (πΉβπ) β Ο |
35 | | nnord 7865 |
. . . . . . . . . 10
β’ ((πΉβπ) β Ο β Ord (πΉβπ)) |
36 | 34, 35 | ax-mp 5 |
. . . . . . . . 9
β’ Ord
(πΉβπ) |
37 | 32, 33 | f0cli 7099 |
. . . . . . . . . 10
β’ (πΉβπ΄) β Ο |
38 | | nnord 7865 |
. . . . . . . . . 10
β’ ((πΉβπ΄) β Ο β Ord (πΉβπ΄)) |
39 | 37, 38 | ax-mp 5 |
. . . . . . . . 9
β’ Ord
(πΉβπ΄) |
40 | | ordsucsssuc 7813 |
. . . . . . . . 9
β’ ((Ord
(πΉβπ) β§ Ord (πΉβπ΄)) β ((πΉβπ) β (πΉβπ΄) β suc (πΉβπ) β suc (πΉβπ΄))) |
41 | 36, 39, 40 | mp2an 690 |
. . . . . . . 8
β’ ((πΉβπ) β (πΉβπ΄) β suc (πΉβπ) β suc (πΉβπ΄)) |
42 | 31, 41 | sylib 217 |
. . . . . . 7
β’ ((π΄ β Ο β§ π β π« π΄) β suc (πΉβπ) β suc (πΉβπ΄)) |
43 | 1 | ackbij1lem14 10230 |
. . . . . . . . 9
β’ (π΄ β Ο β (πΉβ{π΄}) = suc (πΉβπ΄)) |
44 | 1 | ackbij1lem8 10224 |
. . . . . . . . 9
β’ (π΄ β Ο β (πΉβ{π΄}) = (cardβπ« π΄)) |
45 | 43, 44 | eqtr3d 2774 |
. . . . . . . 8
β’ (π΄ β Ο β suc
(πΉβπ΄) = (cardβπ« π΄)) |
46 | 45 | adantr 481 |
. . . . . . 7
β’ ((π΄ β Ο β§ π β π« π΄) β suc (πΉβπ΄) = (cardβπ« π΄)) |
47 | 42, 46 | sseqtrd 4022 |
. . . . . 6
β’ ((π΄ β Ο β§ π β π« π΄) β suc (πΉβπ) β (cardβπ« π΄)) |
48 | | sucssel 6459 |
. . . . . 6
β’ ((πΉβπ) β V β (suc (πΉβπ) β (cardβπ« π΄) β (πΉβπ) β (cardβπ« π΄))) |
49 | 27, 47, 48 | mpsyl 68 |
. . . . 5
β’ ((π΄ β Ο β§ π β π« π΄) β (πΉβπ) β (cardβπ« π΄)) |
50 | 49 | ralrimiva 3146 |
. . . 4
β’ (π΄ β Ο β
βπ β π«
π΄(πΉβπ) β (cardβπ« π΄)) |
51 | | f1fun 6789 |
. . . . . 6
β’ (πΉ:(π« Ο β©
Fin)β1-1βΟ β Fun
πΉ) |
52 | 2, 51 | ax-mp 5 |
. . . . 5
β’ Fun πΉ |
53 | | f1dm 6791 |
. . . . . . 7
β’ (πΉ:(π« Ο β©
Fin)β1-1βΟ β dom
πΉ = (π« Ο
β© Fin)) |
54 | 2, 53 | ax-mp 5 |
. . . . . 6
β’ dom πΉ = (π« Ο β©
Fin) |
55 | 3, 54 | sseqtrrdi 4033 |
. . . . 5
β’ (π΄ β Ο β π«
π΄ β dom πΉ) |
56 | | funimass4 6956 |
. . . . 5
β’ ((Fun
πΉ β§ π« π΄ β dom πΉ) β ((πΉ β π« π΄) β (cardβπ« π΄) β βπ β π« π΄(πΉβπ) β (cardβπ« π΄))) |
57 | 52, 55, 56 | sylancr 587 |
. . . 4
β’ (π΄ β Ο β ((πΉ β π« π΄) β (cardβπ«
π΄) β βπ β π« π΄(πΉβπ) β (cardβπ« π΄))) |
58 | 50, 57 | mpbird 256 |
. . 3
β’ (π΄ β Ο β (πΉ β π« π΄) β (cardβπ«
π΄)) |
59 | | sspss 4099 |
. . 3
β’ ((πΉ β π« π΄) β (cardβπ«
π΄) β ((πΉ β π« π΄) β (cardβπ«
π΄) β¨ (πΉ β π« π΄) = (cardβπ« π΄))) |
60 | 58, 59 | sylib 217 |
. 2
β’ (π΄ β Ο β ((πΉ β π« π΄) β (cardβπ«
π΄) β¨ (πΉ β π« π΄) = (cardβπ« π΄))) |
61 | | orel1 887 |
. 2
β’ (Β¬
(πΉ β π« π΄) β (cardβπ«
π΄) β (((πΉ β π« π΄) β (cardβπ«
π΄) β¨ (πΉ β π« π΄) = (cardβπ« π΄)) β (πΉ β π« π΄) = (cardβπ« π΄))) |
62 | 26, 60, 61 | sylc 65 |
1
β’ (π΄ β Ο β (πΉ β π« π΄) = (cardβπ« π΄)) |