Step | Hyp | Ref
| Expression |
1 | | difss 4132 |
. . . 4
β’ (π΄ β β© (Ο β π΄)) β π΄ |
2 | | ackbij.f |
. . . . 5
β’ πΉ = (π₯ β (π« Ο β© Fin) β¦
(cardββͺ π¦ β π₯ ({π¦} Γ π« π¦))) |
3 | 2 | ackbij1lem11 10228 |
. . . 4
β’ ((π΄ β (π« Ο β©
Fin) β§ (π΄ β β© (Ο β π΄)) β π΄) β (π΄ β β©
(Ο β π΄)) β
(π« Ο β© Fin)) |
4 | 1, 3 | mpan2 688 |
. . 3
β’ (π΄ β (π« Ο β©
Fin) β (π΄ β
β© (Ο β π΄)) β (π« Ο β©
Fin)) |
5 | | difss 4132 |
. . . . . . 7
β’ (Ο
β π΄) β
Ο |
6 | | omsson 7862 |
. . . . . . 7
β’ Ο
β On |
7 | 5, 6 | sstri 3992 |
. . . . . 6
β’ (Ο
β π΄) β
On |
8 | | ominf 9261 |
. . . . . . . 8
β’ Β¬
Ο β Fin |
9 | | elinel2 4197 |
. . . . . . . 8
β’ (π΄ β (π« Ο β©
Fin) β π΄ β
Fin) |
10 | | difinf 9319 |
. . . . . . . 8
β’ ((Β¬
Ο β Fin β§ π΄
β Fin) β Β¬ (Ο β π΄) β Fin) |
11 | 8, 9, 10 | sylancr 586 |
. . . . . . 7
β’ (π΄ β (π« Ο β©
Fin) β Β¬ (Ο β π΄) β Fin) |
12 | | 0fin 9174 |
. . . . . . . . 9
β’ β
β Fin |
13 | | eleq1 2820 |
. . . . . . . . 9
β’ ((Ο
β π΄) = β
β
((Ο β π΄) β
Fin β β
β Fin)) |
14 | 12, 13 | mpbiri 257 |
. . . . . . . 8
β’ ((Ο
β π΄) = β
β
(Ο β π΄) β
Fin) |
15 | 14 | necon3bi 2966 |
. . . . . . 7
β’ (Β¬
(Ο β π΄) β
Fin β (Ο β π΄) β β
) |
16 | 11, 15 | syl 17 |
. . . . . 6
β’ (π΄ β (π« Ο β©
Fin) β (Ο β π΄) β β
) |
17 | | onint 7781 |
. . . . . 6
β’
(((Ο β π΄) β On β§ (Ο β π΄) β β
) β β© (Ο β π΄) β (Ο β π΄)) |
18 | 7, 16, 17 | sylancr 586 |
. . . . 5
β’ (π΄ β (π« Ο β©
Fin) β β© (Ο β π΄) β (Ο β π΄)) |
19 | 18 | eldifad 3961 |
. . . 4
β’ (π΄ β (π« Ο β©
Fin) β β© (Ο β π΄) β Ο) |
20 | | ackbij1lem4 10221 |
. . . 4
β’ (β© (Ο β π΄) β Ο β {β© (Ο β π΄)} β (π« Ο β©
Fin)) |
21 | 19, 20 | syl 17 |
. . 3
β’ (π΄ β (π« Ο β©
Fin) β {β© (Ο β π΄)} β (π« Ο β©
Fin)) |
22 | | ackbij1lem6 10223 |
. . 3
β’ (((π΄ β β© (Ο β π΄)) β (π« Ο β© Fin)
β§ {β© (Ο β π΄)} β (π« Ο β© Fin))
β ((π΄ β β© (Ο β π΄)) βͺ {β©
(Ο β π΄)})
β (π« Ο β© Fin)) |
23 | 4, 21, 22 | syl2anc 583 |
. 2
β’ (π΄ β (π« Ο β©
Fin) β ((π΄ β
β© (Ο β π΄)) βͺ {β©
(Ο β π΄)})
β (π« Ο β© Fin)) |
24 | 18 | eldifbd 3962 |
. . . . . 6
β’ (π΄ β (π« Ο β©
Fin) β Β¬ β© (Ο β π΄) β π΄) |
25 | | disjsn 4716 |
. . . . . 6
β’ ((π΄ β© {β© (Ο β π΄)}) = β
β Β¬ β© (Ο β π΄) β π΄) |
26 | 24, 25 | sylibr 233 |
. . . . 5
β’ (π΄ β (π« Ο β©
Fin) β (π΄ β© {β© (Ο β π΄)}) = β
) |
27 | | ssdisj 4460 |
. . . . 5
β’ (((π΄ β β© (Ο β π΄)) β π΄ β§ (π΄ β© {β©
(Ο β π΄)}) =
β
) β ((π΄ β
β© (Ο β π΄)) β© {β©
(Ο β π΄)}) =
β
) |
28 | 1, 26, 27 | sylancr 586 |
. . . 4
β’ (π΄ β (π« Ο β©
Fin) β ((π΄ β
β© (Ο β π΄)) β© {β©
(Ο β π΄)}) =
β
) |
29 | 2 | ackbij1lem9 10226 |
. . . 4
β’ (((π΄ β β© (Ο β π΄)) β (π« Ο β© Fin)
β§ {β© (Ο β π΄)} β (π« Ο β© Fin)
β§ ((π΄ β β© (Ο β π΄)) β© {β©
(Ο β π΄)}) =
β
) β (πΉβ((π΄ β β©
(Ο β π΄)) βͺ
{β© (Ο β π΄)})) = ((πΉβ(π΄ β β©
(Ο β π΄)))
+o (πΉβ{β©
(Ο β π΄)}))) |
30 | 4, 21, 28, 29 | syl3anc 1370 |
. . 3
β’ (π΄ β (π« Ο β©
Fin) β (πΉβ((π΄ β β©
(Ο β π΄)) βͺ
{β© (Ο β π΄)})) = ((πΉβ(π΄ β β©
(Ο β π΄)))
+o (πΉβ{β©
(Ο β π΄)}))) |
31 | 2 | ackbij1lem14 10231 |
. . . . 5
β’ (β© (Ο β π΄) β Ο β (πΉβ{β©
(Ο β π΄)}) = suc
(πΉββ© (Ο β π΄))) |
32 | 19, 31 | syl 17 |
. . . 4
β’ (π΄ β (π« Ο β©
Fin) β (πΉβ{β© (Ο β π΄)}) = suc (πΉββ© (Ο
β π΄))) |
33 | 32 | oveq2d 7428 |
. . 3
β’ (π΄ β (π« Ο β©
Fin) β ((πΉβ(π΄ β β©
(Ο β π΄)))
+o (πΉβ{β©
(Ο β π΄)})) =
((πΉβ(π΄ β β© (Ο β π΄))) +o suc (πΉββ© (Ο
β π΄)))) |
34 | 2 | ackbij1lem10 10227 |
. . . . . . 7
β’ πΉ:(π« Ο β©
Fin)βΆΟ |
35 | 34 | ffvelcdmi 7086 |
. . . . . 6
β’ ((π΄ β β© (Ο β π΄)) β (π« Ο β© Fin)
β (πΉβ(π΄ β β© (Ο β π΄))) β Ο) |
36 | 4, 35 | syl 17 |
. . . . 5
β’ (π΄ β (π« Ο β©
Fin) β (πΉβ(π΄ β β© (Ο β π΄))) β Ο) |
37 | | ackbij1lem3 10220 |
. . . . . . 7
β’ (β© (Ο β π΄) β Ο β β© (Ο β π΄) β (π« Ο β©
Fin)) |
38 | 19, 37 | syl 17 |
. . . . . 6
β’ (π΄ β (π« Ο β©
Fin) β β© (Ο β π΄) β (π« Ο β©
Fin)) |
39 | 34 | ffvelcdmi 7086 |
. . . . . 6
β’ (β© (Ο β π΄) β (π« Ο β© Fin)
β (πΉββ© (Ο β π΄)) β Ο) |
40 | 38, 39 | syl 17 |
. . . . 5
β’ (π΄ β (π« Ο β©
Fin) β (πΉββ© (Ο β π΄)) β Ο) |
41 | | nnasuc 8609 |
. . . . 5
β’ (((πΉβ(π΄ β β©
(Ο β π΄)))
β Ο β§ (πΉββ© (Ο
β π΄)) β Ο)
β ((πΉβ(π΄ β β© (Ο β π΄))) +o suc (πΉββ© (Ο
β π΄))) = suc ((πΉβ(π΄ β β©
(Ο β π΄)))
+o (πΉββ© (Ο
β π΄)))) |
42 | 36, 40, 41 | syl2anc 583 |
. . . 4
β’ (π΄ β (π« Ο β©
Fin) β ((πΉβ(π΄ β β©
(Ο β π΄)))
+o suc (πΉββ© (Ο
β π΄))) = suc ((πΉβ(π΄ β β©
(Ο β π΄)))
+o (πΉββ© (Ο
β π΄)))) |
43 | | disjdifr 4473 |
. . . . . . . 8
β’ ((π΄ β β© (Ο β π΄)) β© β©
(Ο β π΄)) =
β
|
44 | 43 | a1i 11 |
. . . . . . 7
β’ (π΄ β (π« Ο β©
Fin) β ((π΄ β
β© (Ο β π΄)) β© β©
(Ο β π΄)) =
β
) |
45 | 2 | ackbij1lem9 10226 |
. . . . . . 7
β’ (((π΄ β β© (Ο β π΄)) β (π« Ο β© Fin)
β§ β© (Ο β π΄) β (π« Ο β© Fin) β§
((π΄ β β© (Ο β π΄)) β© β©
(Ο β π΄)) =
β
) β (πΉβ((π΄ β β©
(Ο β π΄)) βͺ
β© (Ο β π΄))) = ((πΉβ(π΄ β β©
(Ο β π΄)))
+o (πΉββ© (Ο
β π΄)))) |
46 | 4, 38, 44, 45 | syl3anc 1370 |
. . . . . 6
β’ (π΄ β (π« Ο β©
Fin) β (πΉβ((π΄ β β©
(Ο β π΄)) βͺ
β© (Ο β π΄))) = ((πΉβ(π΄ β β©
(Ο β π΄)))
+o (πΉββ© (Ο
β π΄)))) |
47 | | uncom 4154 |
. . . . . . . 8
β’ ((π΄ β β© (Ο β π΄)) βͺ β©
(Ο β π΄)) =
(β© (Ο β π΄) βͺ (π΄ β β©
(Ο β π΄))) |
48 | | onnmin 7789 |
. . . . . . . . . . . . . . 15
β’
(((Ο β π΄) β On β§ π β (Ο β π΄)) β Β¬ π β β© (Ο
β π΄)) |
49 | 7, 48 | mpan 687 |
. . . . . . . . . . . . . 14
β’ (π β (Ο β π΄) β Β¬ π β β© (Ο β π΄)) |
50 | 49 | con2i 139 |
. . . . . . . . . . . . 13
β’ (π β β© (Ο β π΄) β Β¬ π β (Ο β π΄)) |
51 | 50 | adantl 481 |
. . . . . . . . . . . 12
β’ ((π΄ β (π« Ο β©
Fin) β§ π β β© (Ο β π΄)) β Β¬ π β (Ο β π΄)) |
52 | | ordom 7868 |
. . . . . . . . . . . . . . 15
β’ Ord
Ο |
53 | | ordelss 6381 |
. . . . . . . . . . . . . . 15
β’ ((Ord
Ο β§ β© (Ο β π΄) β Ο) β β© (Ο β π΄) β Ο) |
54 | 52, 19, 53 | sylancr 586 |
. . . . . . . . . . . . . 14
β’ (π΄ β (π« Ο β©
Fin) β β© (Ο β π΄) β Ο) |
55 | 54 | sselda 3983 |
. . . . . . . . . . . . 13
β’ ((π΄ β (π« Ο β©
Fin) β§ π β β© (Ο β π΄)) β π β Ο) |
56 | | eldif 3959 |
. . . . . . . . . . . . . . . 16
β’ (π β (Ο β π΄) β (π β Ο β§ Β¬ π β π΄)) |
57 | 56 | simplbi2 500 |
. . . . . . . . . . . . . . 15
β’ (π β Ο β (Β¬
π β π΄ β π β (Ο β π΄))) |
58 | 57 | orrd 860 |
. . . . . . . . . . . . . 14
β’ (π β Ο β (π β π΄ β¨ π β (Ο β π΄))) |
59 | 58 | orcomd 868 |
. . . . . . . . . . . . 13
β’ (π β Ο β (π β (Ο β π΄) β¨ π β π΄)) |
60 | 55, 59 | syl 17 |
. . . . . . . . . . . 12
β’ ((π΄ β (π« Ο β©
Fin) β§ π β β© (Ο β π΄)) β (π β (Ο β π΄) β¨ π β π΄)) |
61 | | orel1 886 |
. . . . . . . . . . . 12
β’ (Β¬
π β (Ο β
π΄) β ((π β (Ο β π΄) β¨ π β π΄) β π β π΄)) |
62 | 51, 60, 61 | sylc 65 |
. . . . . . . . . . 11
β’ ((π΄ β (π« Ο β©
Fin) β§ π β β© (Ο β π΄)) β π β π΄) |
63 | 62 | ex 412 |
. . . . . . . . . 10
β’ (π΄ β (π« Ο β©
Fin) β (π β β© (Ο β π΄) β π β π΄)) |
64 | 63 | ssrdv 3989 |
. . . . . . . . 9
β’ (π΄ β (π« Ο β©
Fin) β β© (Ο β π΄) β π΄) |
65 | | undif 4482 |
. . . . . . . . 9
β’ (β© (Ο β π΄) β π΄ β (β©
(Ο β π΄) βͺ
(π΄ β β© (Ο β π΄))) = π΄) |
66 | 64, 65 | sylib 217 |
. . . . . . . 8
β’ (π΄ β (π« Ο β©
Fin) β (β© (Ο β π΄) βͺ (π΄ β β©
(Ο β π΄))) =
π΄) |
67 | 47, 66 | eqtrid 2783 |
. . . . . . 7
β’ (π΄ β (π« Ο β©
Fin) β ((π΄ β
β© (Ο β π΄)) βͺ β©
(Ο β π΄)) =
π΄) |
68 | 67 | fveq2d 6896 |
. . . . . 6
β’ (π΄ β (π« Ο β©
Fin) β (πΉβ((π΄ β β©
(Ο β π΄)) βͺ
β© (Ο β π΄))) = (πΉβπ΄)) |
69 | 46, 68 | eqtr3d 2773 |
. . . . 5
β’ (π΄ β (π« Ο β©
Fin) β ((πΉβ(π΄ β β©
(Ο β π΄)))
+o (πΉββ© (Ο
β π΄))) = (πΉβπ΄)) |
70 | | suceq 6431 |
. . . . 5
β’ (((πΉβ(π΄ β β©
(Ο β π΄)))
+o (πΉββ© (Ο
β π΄))) = (πΉβπ΄) β suc ((πΉβ(π΄ β β©
(Ο β π΄)))
+o (πΉββ© (Ο
β π΄))) = suc (πΉβπ΄)) |
71 | 69, 70 | syl 17 |
. . . 4
β’ (π΄ β (π« Ο β©
Fin) β suc ((πΉβ(π΄ β β©
(Ο β π΄)))
+o (πΉββ© (Ο
β π΄))) = suc (πΉβπ΄)) |
72 | 42, 71 | eqtrd 2771 |
. . 3
β’ (π΄ β (π« Ο β©
Fin) β ((πΉβ(π΄ β β©
(Ο β π΄)))
+o suc (πΉββ© (Ο
β π΄))) = suc (πΉβπ΄)) |
73 | 30, 33, 72 | 3eqtrd 2775 |
. 2
β’ (π΄ β (π« Ο β©
Fin) β (πΉβ((π΄ β β©
(Ο β π΄)) βͺ
{β© (Ο β π΄)})) = suc (πΉβπ΄)) |
74 | | fveqeq2 6901 |
. . 3
β’ (π = ((π΄ β β©
(Ο β π΄)) βͺ
{β© (Ο β π΄)}) β ((πΉβπ) = suc (πΉβπ΄) β (πΉβ((π΄ β β©
(Ο β π΄)) βͺ
{β© (Ο β π΄)})) = suc (πΉβπ΄))) |
75 | 74 | rspcev 3613 |
. 2
β’ ((((π΄ β β© (Ο β π΄)) βͺ {β©
(Ο β π΄)})
β (π« Ο β© Fin) β§ (πΉβ((π΄ β β©
(Ο β π΄)) βͺ
{β© (Ο β π΄)})) = suc (πΉβπ΄)) β βπ β (π« Ο β© Fin)(πΉβπ) = suc (πΉβπ΄)) |
76 | 23, 73, 75 | syl2anc 583 |
1
β’ (π΄ β (π« Ο β©
Fin) β βπ β
(π« Ο β© Fin)(πΉβπ) = suc (πΉβπ΄)) |