Step | Hyp | Ref
| Expression |
1 | | f1rel 5426 |
. . . 4
β’ (πΉ:π΄β1-1βπ΅ β Rel πΉ) |
2 | 1 | ad2antlr 489 |
. . 3
β’ (((π΄ β π β§ πΉ:π΄β1-1βπ΅) β§ πΉ β Fin) β Rel πΉ) |
3 | | f1cnv 5486 |
. . . . 5
β’ (πΉ:π΄β1-1βπ΅ β β‘πΉ:ran πΉβ1-1-ontoβπ΄) |
4 | | f1ofun 5464 |
. . . . 5
β’ (β‘πΉ:ran πΉβ1-1-ontoβπ΄ β Fun β‘πΉ) |
5 | 3, 4 | syl 14 |
. . . 4
β’ (πΉ:π΄β1-1βπ΅ β Fun β‘πΉ) |
6 | 5 | ad2antlr 489 |
. . 3
β’ (((π΄ β π β§ πΉ:π΄β1-1βπ΅) β§ πΉ β Fin) β Fun β‘πΉ) |
7 | | simpr 110 |
. . 3
β’ (((π΄ β π β§ πΉ:π΄β1-1βπ΅) β§ πΉ β Fin) β πΉ β Fin) |
8 | | funrnfi 6941 |
. . 3
β’ ((Rel
πΉ β§ Fun β‘πΉ β§ πΉ β Fin) β ran πΉ β Fin) |
9 | 2, 6, 7, 8 | syl3anc 1238 |
. 2
β’ (((π΄ β π β§ πΉ:π΄β1-1βπ΅) β§ πΉ β Fin) β ran πΉ β Fin) |
10 | | simpr 110 |
. . . 4
β’ (((π΄ β π β§ πΉ:π΄β1-1βπ΅) β§ ran πΉ β Fin) β ran πΉ β Fin) |
11 | | f1dm 5427 |
. . . . . . . 8
β’ (πΉ:π΄β1-1βπ΅ β dom πΉ = π΄) |
12 | | f1f1orn 5473 |
. . . . . . . 8
β’ (πΉ:π΄β1-1βπ΅ β πΉ:π΄β1-1-ontoβran
πΉ) |
13 | | eleq1 2240 |
. . . . . . . . . . . 12
β’ (π΄ = dom πΉ β (π΄ β π β dom πΉ β π)) |
14 | | f1oeq2 5451 |
. . . . . . . . . . . 12
β’ (π΄ = dom πΉ β (πΉ:π΄β1-1-ontoβran
πΉ β πΉ:dom πΉβ1-1-ontoβran
πΉ)) |
15 | 13, 14 | anbi12d 473 |
. . . . . . . . . . 11
β’ (π΄ = dom πΉ β ((π΄ β π β§ πΉ:π΄β1-1-ontoβran
πΉ) β (dom πΉ β π β§ πΉ:dom πΉβ1-1-ontoβran
πΉ))) |
16 | 15 | eqcoms 2180 |
. . . . . . . . . 10
β’ (dom
πΉ = π΄ β ((π΄ β π β§ πΉ:π΄β1-1-ontoβran
πΉ) β (dom πΉ β π β§ πΉ:dom πΉβ1-1-ontoβran
πΉ))) |
17 | 16 | biimpd 144 |
. . . . . . . . 9
β’ (dom
πΉ = π΄ β ((π΄ β π β§ πΉ:π΄β1-1-ontoβran
πΉ) β (dom πΉ β π β§ πΉ:dom πΉβ1-1-ontoβran
πΉ))) |
18 | 17 | expcomd 1441 |
. . . . . . . 8
β’ (dom
πΉ = π΄ β (πΉ:π΄β1-1-ontoβran
πΉ β (π΄ β π β (dom πΉ β π β§ πΉ:dom πΉβ1-1-ontoβran
πΉ)))) |
19 | 11, 12, 18 | sylc 62 |
. . . . . . 7
β’ (πΉ:π΄β1-1βπ΅ β (π΄ β π β (dom πΉ β π β§ πΉ:dom πΉβ1-1-ontoβran
πΉ))) |
20 | 19 | impcom 125 |
. . . . . 6
β’ ((π΄ β π β§ πΉ:π΄β1-1βπ΅) β (dom πΉ β π β§ πΉ:dom πΉβ1-1-ontoβran
πΉ)) |
21 | 20 | adantr 276 |
. . . . 5
β’ (((π΄ β π β§ πΉ:π΄β1-1βπ΅) β§ ran πΉ β Fin) β (dom πΉ β π β§ πΉ:dom πΉβ1-1-ontoβran
πΉ)) |
22 | | f1oeng 6757 |
. . . . 5
β’ ((dom
πΉ β π β§ πΉ:dom πΉβ1-1-ontoβran
πΉ) β dom πΉ β ran πΉ) |
23 | 21, 22 | syl 14 |
. . . 4
β’ (((π΄ β π β§ πΉ:π΄β1-1βπ΅) β§ ran πΉ β Fin) β dom πΉ β ran πΉ) |
24 | | enfii 6874 |
. . . 4
β’ ((ran
πΉ β Fin β§ dom
πΉ β ran πΉ) β dom πΉ β Fin) |
25 | 10, 23, 24 | syl2anc 411 |
. . 3
β’ (((π΄ β π β§ πΉ:π΄β1-1βπ΅) β§ ran πΉ β Fin) β dom πΉ β Fin) |
26 | | f1fun 5425 |
. . . . 5
β’ (πΉ:π΄β1-1βπ΅ β Fun πΉ) |
27 | 26 | ad2antlr 489 |
. . . 4
β’ (((π΄ β π β§ πΉ:π΄β1-1βπ΅) β§ ran πΉ β Fin) β Fun πΉ) |
28 | | fundmfibi 6938 |
. . . 4
β’ (Fun
πΉ β (πΉ β Fin β dom πΉ β Fin)) |
29 | 27, 28 | syl 14 |
. . 3
β’ (((π΄ β π β§ πΉ:π΄β1-1βπ΅) β§ ran πΉ β Fin) β (πΉ β Fin β dom πΉ β Fin)) |
30 | 25, 29 | mpbird 167 |
. 2
β’ (((π΄ β π β§ πΉ:π΄β1-1βπ΅) β§ ran πΉ β Fin) β πΉ β Fin) |
31 | 9, 30 | impbida 596 |
1
β’ ((π΄ β π β§ πΉ:π΄β1-1βπ΅) β (πΉ β Fin β ran πΉ β Fin)) |