Step | Hyp | Ref
| Expression |
1 | | fin23lem.a |
. . 3
β’ π = seqΟ((π β Ο, π’ β V β¦ if(((π‘βπ) β© π’) = β
, π’, ((π‘βπ) β© π’))), βͺ ran π‘) |
2 | | fin23lem17.f |
. . 3
β’ πΉ = {π β£ βπ β (π« π βm Ο)(βπ₯ β Ο (πβsuc π₯) β (πβπ₯) β β© ran
π β ran π)} |
3 | 1, 2 | fin23lem17 10282 |
. 2
β’ ((βͺ ran π‘ β πΉ β§ π‘:Οβ1-1βπ) β β© ran
π β ran π) |
4 | 1 | fnseqom 8405 |
. . . . 5
β’ π Fn Ο |
5 | | fvelrnb 6907 |
. . . . 5
β’ (π Fn Ο β (β© ran π β ran π β βπ β Ο (πβπ) = β© ran π)) |
6 | 4, 5 | ax-mp 5 |
. . . 4
β’ (β© ran π β ran π β βπ β Ο (πβπ) = β© ran π) |
7 | | id 22 |
. . . . . . 7
β’ (π β Ο β π β
Ο) |
8 | | vex 3451 |
. . . . . . . . . 10
β’ π‘ β V |
9 | | f1f1orn 6799 |
. . . . . . . . . 10
β’ (π‘:Οβ1-1βπ β π‘:Οβ1-1-ontoβran
π‘) |
10 | | f1oen3g 8912 |
. . . . . . . . . 10
β’ ((π‘ β V β§ π‘:Οβ1-1-ontoβran
π‘) β Ο β
ran π‘) |
11 | 8, 9, 10 | sylancr 588 |
. . . . . . . . 9
β’ (π‘:Οβ1-1βπ β Ο β ran π‘) |
12 | | ominf 9208 |
. . . . . . . . 9
β’ Β¬
Ο β Fin |
13 | | ssdif0 4327 |
. . . . . . . . . . 11
β’ (ran
π‘ β {β
} β
(ran π‘ β {β
}) =
β
) |
14 | | snfi 8994 |
. . . . . . . . . . . . 13
β’ {β
}
β Fin |
15 | | ssfi 9123 |
. . . . . . . . . . . . 13
β’
(({β
} β Fin β§ ran π‘ β {β
}) β ran π‘ β Fin) |
16 | 14, 15 | mpan 689 |
. . . . . . . . . . . 12
β’ (ran
π‘ β {β
} β
ran π‘ β
Fin) |
17 | | enfi 9140 |
. . . . . . . . . . . 12
β’ (Ο
β ran π‘ β
(Ο β Fin β ran π‘ β Fin)) |
18 | 16, 17 | imbitrrid 245 |
. . . . . . . . . . 11
β’ (Ο
β ran π‘ β (ran
π‘ β {β
} β
Ο β Fin)) |
19 | 13, 18 | biimtrrid 242 |
. . . . . . . . . 10
β’ (Ο
β ran π‘ β ((ran
π‘ β {β
}) =
β
β Ο β Fin)) |
20 | 19 | necon3bd 2954 |
. . . . . . . . 9
β’ (Ο
β ran π‘ β (Β¬
Ο β Fin β (ran π‘ β {β
}) β
β
)) |
21 | 11, 12, 20 | mpisyl 21 |
. . . . . . . 8
β’ (π‘:Οβ1-1βπ β (ran π‘ β {β
}) β
β
) |
22 | | n0 4310 |
. . . . . . . . 9
β’ ((ran
π‘ β {β
}) β
β
β βπ
π β (ran π‘ β
{β
})) |
23 | | eldifsn 4751 |
. . . . . . . . . . 11
β’ (π β (ran π‘ β {β
}) β (π β ran π‘ β§ π β β
)) |
24 | | elssuni 4902 |
. . . . . . . . . . . 12
β’ (π β ran π‘ β π β βͺ ran
π‘) |
25 | | ssn0 4364 |
. . . . . . . . . . . 12
β’ ((π β βͺ ran π‘ β§ π β β
) β βͺ ran π‘ β β
) |
26 | 24, 25 | sylan 581 |
. . . . . . . . . . 11
β’ ((π β ran π‘ β§ π β β
) β βͺ ran π‘ β β
) |
27 | 23, 26 | sylbi 216 |
. . . . . . . . . 10
β’ (π β (ran π‘ β {β
}) β βͺ ran π‘ β β
) |
28 | 27 | exlimiv 1934 |
. . . . . . . . 9
β’
(βπ π β (ran π‘ β {β
}) β βͺ ran π‘ β β
) |
29 | 22, 28 | sylbi 216 |
. . . . . . . 8
β’ ((ran
π‘ β {β
}) β
β
β βͺ ran π‘ β β
) |
30 | 21, 29 | syl 17 |
. . . . . . 7
β’ (π‘:Οβ1-1βπ β βͺ ran
π‘ β
β
) |
31 | 1 | fin23lem14 10277 |
. . . . . . 7
β’ ((π β Ο β§ βͺ ran π‘ β β
) β (πβπ) β β
) |
32 | 7, 30, 31 | syl2anr 598 |
. . . . . 6
β’ ((π‘:Οβ1-1βπ β§ π β Ο) β (πβπ) β β
) |
33 | | neeq1 3003 |
. . . . . 6
β’ ((πβπ) = β© ran π β ((πβπ) β β
β β© ran π β β
)) |
34 | 32, 33 | syl5ibcom 244 |
. . . . 5
β’ ((π‘:Οβ1-1βπ β§ π β Ο) β ((πβπ) = β© ran π β β© ran π β β
)) |
35 | 34 | rexlimdva 3149 |
. . . 4
β’ (π‘:Οβ1-1βπ β (βπ β Ο (πβπ) = β© ran π β β© ran π β β
)) |
36 | 6, 35 | biimtrid 241 |
. . 3
β’ (π‘:Οβ1-1βπ β (β© ran
π β ran π β β© ran π β β
)) |
37 | 36 | adantl 483 |
. 2
β’ ((βͺ ran π‘ β πΉ β§ π‘:Οβ1-1βπ) β (β© ran
π β ran π β β© ran π β β
)) |
38 | 3, 37 | mpd 15 |
1
β’ ((βͺ ran π‘ β πΉ β§ π‘:Οβ1-1βπ) β β© ran
π β
β
) |