Step | Hyp | Ref
| Expression |
1 | | rnfi 9335 |
. 2
β’ (πΉ β Fin β ran πΉ β Fin) |
2 | | simpr 486 |
. . . . 5
β’ (((π΄ β π β§ πΉ:π΄β1-1βπ΅) β§ ran πΉ β Fin) β ran πΉ β Fin) |
3 | | f1dm 6792 |
. . . . . . . . 9
β’ (πΉ:π΄β1-1βπ΅ β dom πΉ = π΄) |
4 | | f1f1orn 6845 |
. . . . . . . . 9
β’ (πΉ:π΄β1-1βπ΅ β πΉ:π΄β1-1-ontoβran
πΉ) |
5 | | eleq1 2822 |
. . . . . . . . . . . . 13
β’ (π΄ = dom πΉ β (π΄ β π β dom πΉ β π)) |
6 | | f1oeq2 6823 |
. . . . . . . . . . . . 13
β’ (π΄ = dom πΉ β (πΉ:π΄β1-1-ontoβran
πΉ β πΉ:dom πΉβ1-1-ontoβran
πΉ)) |
7 | 5, 6 | anbi12d 632 |
. . . . . . . . . . . 12
β’ (π΄ = dom πΉ β ((π΄ β π β§ πΉ:π΄β1-1-ontoβran
πΉ) β (dom πΉ β π β§ πΉ:dom πΉβ1-1-ontoβran
πΉ))) |
8 | 7 | eqcoms 2741 |
. . . . . . . . . . 11
β’ (dom
πΉ = π΄ β ((π΄ β π β§ πΉ:π΄β1-1-ontoβran
πΉ) β (dom πΉ β π β§ πΉ:dom πΉβ1-1-ontoβran
πΉ))) |
9 | 8 | biimpd 228 |
. . . . . . . . . 10
β’ (dom
πΉ = π΄ β ((π΄ β π β§ πΉ:π΄β1-1-ontoβran
πΉ) β (dom πΉ β π β§ πΉ:dom πΉβ1-1-ontoβran
πΉ))) |
10 | 9 | expcomd 418 |
. . . . . . . . 9
β’ (dom
πΉ = π΄ β (πΉ:π΄β1-1-ontoβran
πΉ β (π΄ β π β (dom πΉ β π β§ πΉ:dom πΉβ1-1-ontoβran
πΉ)))) |
11 | 3, 4, 10 | sylc 65 |
. . . . . . . 8
β’ (πΉ:π΄β1-1βπ΅ β (π΄ β π β (dom πΉ β π β§ πΉ:dom πΉβ1-1-ontoβran
πΉ))) |
12 | 11 | impcom 409 |
. . . . . . 7
β’ ((π΄ β π β§ πΉ:π΄β1-1βπ΅) β (dom πΉ β π β§ πΉ:dom πΉβ1-1-ontoβran
πΉ)) |
13 | 12 | adantr 482 |
. . . . . 6
β’ (((π΄ β π β§ πΉ:π΄β1-1βπ΅) β§ ran πΉ β Fin) β (dom πΉ β π β§ πΉ:dom πΉβ1-1-ontoβran
πΉ)) |
14 | | f1oeng 8967 |
. . . . . 6
β’ ((dom
πΉ β π β§ πΉ:dom πΉβ1-1-ontoβran
πΉ) β dom πΉ β ran πΉ) |
15 | 13, 14 | syl 17 |
. . . . 5
β’ (((π΄ β π β§ πΉ:π΄β1-1βπ΅) β§ ran πΉ β Fin) β dom πΉ β ran πΉ) |
16 | | enfii 9189 |
. . . . 5
β’ ((ran
πΉ β Fin β§ dom
πΉ β ran πΉ) β dom πΉ β Fin) |
17 | 2, 15, 16 | syl2anc 585 |
. . . 4
β’ (((π΄ β π β§ πΉ:π΄β1-1βπ΅) β§ ran πΉ β Fin) β dom πΉ β Fin) |
18 | | f1fun 6790 |
. . . . . 6
β’ (πΉ:π΄β1-1βπ΅ β Fun πΉ) |
19 | 18 | ad2antlr 726 |
. . . . 5
β’ (((π΄ β π β§ πΉ:π΄β1-1βπ΅) β§ ran πΉ β Fin) β Fun πΉ) |
20 | | fundmfibi 9331 |
. . . . 5
β’ (Fun
πΉ β (πΉ β Fin β dom πΉ β Fin)) |
21 | 19, 20 | syl 17 |
. . . 4
β’ (((π΄ β π β§ πΉ:π΄β1-1βπ΅) β§ ran πΉ β Fin) β (πΉ β Fin β dom πΉ β Fin)) |
22 | 17, 21 | mpbird 257 |
. . 3
β’ (((π΄ β π β§ πΉ:π΄β1-1βπ΅) β§ ran πΉ β Fin) β πΉ β Fin) |
23 | 22 | ex 414 |
. 2
β’ ((π΄ β π β§ πΉ:π΄β1-1βπ΅) β (ran πΉ β Fin β πΉ β Fin)) |
24 | 1, 23 | impbid2 225 |
1
β’ ((π΄ β π β§ πΉ:π΄β1-1βπ΅) β (πΉ β Fin β ran πΉ β Fin)) |