Step | Hyp | Ref
| Expression |
1 | | elmapi 8847 |
. . . 4
β’ (π β (π« π΄ βm Ο)
β π:ΟβΆπ« π΄) |
2 | | simpl 482 |
. . . . . 6
β’ ((π΄ β FinII β§
(π:ΟβΆπ«
π΄ β§ βπ β Ο (πβsuc π) β (πβπ))) β π΄ β FinII) |
3 | | frn 6724 |
. . . . . . 7
β’ (π:ΟβΆπ« π΄ β ran π β π« π΄) |
4 | 3 | ad2antrl 725 |
. . . . . 6
β’ ((π΄ β FinII β§
(π:ΟβΆπ«
π΄ β§ βπ β Ο (πβsuc π) β (πβπ))) β ran π β π« π΄) |
5 | | fdm 6726 |
. . . . . . . . 9
β’ (π:ΟβΆπ« π΄ β dom π = Ο) |
6 | | peano1 7883 |
. . . . . . . . . 10
β’ β
β Ο |
7 | | ne0i 4334 |
. . . . . . . . . 10
β’ (β
β Ο β Ο β β
) |
8 | 6, 7 | mp1i 13 |
. . . . . . . . 9
β’ (π:ΟβΆπ« π΄ β Ο β
β
) |
9 | 5, 8 | eqnetrd 3007 |
. . . . . . . 8
β’ (π:ΟβΆπ« π΄ β dom π β β
) |
10 | | dm0rn0 5924 |
. . . . . . . . 9
β’ (dom
π = β
β ran
π =
β
) |
11 | 10 | necon3bii 2992 |
. . . . . . . 8
β’ (dom
π β β
β ran
π β
β
) |
12 | 9, 11 | sylib 217 |
. . . . . . 7
β’ (π:ΟβΆπ« π΄ β ran π β β
) |
13 | 12 | ad2antrl 725 |
. . . . . 6
β’ ((π΄ β FinII β§
(π:ΟβΆπ«
π΄ β§ βπ β Ο (πβsuc π) β (πβπ))) β ran π β β
) |
14 | | ffn 6717 |
. . . . . . . . 9
β’ (π:ΟβΆπ« π΄ β π Fn Ο) |
15 | 14 | ad2antrl 725 |
. . . . . . . 8
β’ ((π΄ β FinII β§
(π:ΟβΆπ«
π΄ β§ βπ β Ο (πβsuc π) β (πβπ))) β π Fn Ο) |
16 | | sspss 4099 |
. . . . . . . . . . 11
β’ ((πβsuc π) β (πβπ) β ((πβsuc π) β (πβπ) β¨ (πβsuc π) = (πβπ))) |
17 | | fvex 6904 |
. . . . . . . . . . . . . 14
β’ (πβπ) β V |
18 | | fvex 6904 |
. . . . . . . . . . . . . 14
β’ (πβsuc π) β V |
19 | 17, 18 | brcnv 5882 |
. . . . . . . . . . . . 13
β’ ((πβπ)β‘
[β] (πβsuc π) β (πβsuc π) [β] (πβπ)) |
20 | 17 | brrpss 7720 |
. . . . . . . . . . . . 13
β’ ((πβsuc π) [β] (πβπ) β (πβsuc π) β (πβπ)) |
21 | 19, 20 | bitri 275 |
. . . . . . . . . . . 12
β’ ((πβπ)β‘
[β] (πβsuc π) β (πβsuc π) β (πβπ)) |
22 | | eqcom 2738 |
. . . . . . . . . . . 12
β’ ((πβπ) = (πβsuc π) β (πβsuc π) = (πβπ)) |
23 | 21, 22 | orbi12i 912 |
. . . . . . . . . . 11
β’ (((πβπ)β‘
[β] (πβsuc π) β¨ (πβπ) = (πβsuc π)) β ((πβsuc π) β (πβπ) β¨ (πβsuc π) = (πβπ))) |
24 | 16, 23 | sylbb2 237 |
. . . . . . . . . 10
β’ ((πβsuc π) β (πβπ) β ((πβπ)β‘
[β] (πβsuc π) β¨ (πβπ) = (πβsuc π))) |
25 | 24 | ralimi 3082 |
. . . . . . . . 9
β’
(βπ β
Ο (πβsuc π) β (πβπ) β βπ β Ο ((πβπ)β‘
[β] (πβsuc π) β¨ (πβπ) = (πβsuc π))) |
26 | 25 | ad2antll 726 |
. . . . . . . 8
β’ ((π΄ β FinII β§
(π:ΟβΆπ«
π΄ β§ βπ β Ο (πβsuc π) β (πβπ))) β βπ β Ο ((πβπ)β‘
[β] (πβsuc π) β¨ (πβπ) = (πβsuc π))) |
27 | | porpss 7721 |
. . . . . . . . . 10
β’
[β] Po ran π |
28 | | cnvpo 6286 |
. . . . . . . . . 10
β’ (
[β] Po ran π
β β‘ [β] Po ran π) |
29 | 27, 28 | mpbi 229 |
. . . . . . . . 9
β’ β‘ [β] Po ran π |
30 | 29 | a1i 11 |
. . . . . . . 8
β’ ((π΄ β FinII β§
(π:ΟβΆπ«
π΄ β§ βπ β Ο (πβsuc π) β (πβπ))) β β‘ [β] Po ran π) |
31 | | sornom 10276 |
. . . . . . . 8
β’ ((π Fn Ο β§ βπ β Ο ((πβπ)β‘
[β] (πβsuc π) β¨ (πβπ) = (πβsuc π)) β§ β‘ [β] Po ran π) β β‘ [β] Or ran π) |
32 | 15, 26, 30, 31 | syl3anc 1370 |
. . . . . . 7
β’ ((π΄ β FinII β§
(π:ΟβΆπ«
π΄ β§ βπ β Ο (πβsuc π) β (πβπ))) β β‘ [β] Or ran π) |
33 | | cnvso 6287 |
. . . . . . 7
β’ (
[β] Or ran π
β β‘ [β] Or ran π) |
34 | 32, 33 | sylibr 233 |
. . . . . 6
β’ ((π΄ β FinII β§
(π:ΟβΆπ«
π΄ β§ βπ β Ο (πβsuc π) β (πβπ))) β [β] Or ran π) |
35 | | fin2i2 10317 |
. . . . . 6
β’ (((π΄ β FinII β§
ran π β π«
π΄) β§ (ran π β β
β§
[β] Or ran π)) β β© ran
π β ran π) |
36 | 2, 4, 13, 34, 35 | syl22anc 836 |
. . . . 5
β’ ((π΄ β FinII β§
(π:ΟβΆπ«
π΄ β§ βπ β Ο (πβsuc π) β (πβπ))) β β© ran
π β ran π) |
37 | 36 | expr 456 |
. . . 4
β’ ((π΄ β FinII β§
π:ΟβΆπ«
π΄) β (βπ β Ο (πβsuc π) β (πβπ) β β© ran
π β ran π)) |
38 | 1, 37 | sylan2 592 |
. . 3
β’ ((π΄ β FinII β§
π β (π« π΄ βm Ο))
β (βπ β
Ο (πβsuc π) β (πβπ) β β© ran
π β ran π)) |
39 | 38 | ralrimiva 3145 |
. 2
β’ (π΄ β FinII β
βπ β (π«
π΄ βm
Ο)(βπ β
Ο (πβsuc π) β (πβπ) β β© ran
π β ran π)) |
40 | | fin23lem40.f |
. . 3
β’ πΉ = {π β£ βπ β (π« π βm Ο)(βπ₯ β Ο (πβsuc π₯) β (πβπ₯) β β© ran
π β ran π)} |
41 | 40 | isfin3ds 10328 |
. 2
β’ (π΄ β FinII β
(π΄ β πΉ β βπ β (π« π΄ βm Ο)(βπ β Ο (πβsuc π) β (πβπ) β β© ran
π β ran π))) |
42 | 39, 41 | mpbird 257 |
1
β’ (π΄ β FinII β
π΄ β πΉ) |