Step | Hyp | Ref
| Expression |
1 | | df-f 6501 |
. . . 4
β’ (πΉ:π΄βΆπ΅ β (πΉ Fn π΄ β§ ran πΉ β π΅)) |
2 | | dffn4 6763 |
. . . . 5
β’ (πΉ Fn π΄ β πΉ:π΄βontoβran πΉ) |
3 | 2 | anbi1i 625 |
. . . 4
β’ ((πΉ Fn π΄ β§ ran πΉ β π΅) β (πΉ:π΄βontoβran πΉ β§ ran πΉ β π΅)) |
4 | 1, 3 | bitri 275 |
. . 3
β’ (πΉ:π΄βΆπ΅ β (πΉ:π΄βontoβran πΉ β§ ran πΉ β π΅)) |
5 | | f11o.1 |
. . . . 5
β’ πΉ β V |
6 | 5 | rnex 7850 |
. . . 4
β’ ran πΉ β V |
7 | | foeq3 6755 |
. . . . 5
β’ (π₯ = ran πΉ β (πΉ:π΄βontoβπ₯ β πΉ:π΄βontoβran πΉ)) |
8 | | sseq1 3970 |
. . . . 5
β’ (π₯ = ran πΉ β (π₯ β π΅ β ran πΉ β π΅)) |
9 | 7, 8 | anbi12d 632 |
. . . 4
β’ (π₯ = ran πΉ β ((πΉ:π΄βontoβπ₯ β§ π₯ β π΅) β (πΉ:π΄βontoβran πΉ β§ ran πΉ β π΅))) |
10 | 6, 9 | spcev 3564 |
. . 3
β’ ((πΉ:π΄βontoβran πΉ β§ ran πΉ β π΅) β βπ₯(πΉ:π΄βontoβπ₯ β§ π₯ β π΅)) |
11 | 4, 10 | sylbi 216 |
. 2
β’ (πΉ:π΄βΆπ΅ β βπ₯(πΉ:π΄βontoβπ₯ β§ π₯ β π΅)) |
12 | | fof 6757 |
. . . 4
β’ (πΉ:π΄βontoβπ₯ β πΉ:π΄βΆπ₯) |
13 | | fss 6686 |
. . . 4
β’ ((πΉ:π΄βΆπ₯ β§ π₯ β π΅) β πΉ:π΄βΆπ΅) |
14 | 12, 13 | sylan 581 |
. . 3
β’ ((πΉ:π΄βontoβπ₯ β§ π₯ β π΅) β πΉ:π΄βΆπ΅) |
15 | 14 | exlimiv 1934 |
. 2
β’
(βπ₯(πΉ:π΄βontoβπ₯ β§ π₯ β π΅) β πΉ:π΄βΆπ΅) |
16 | 11, 15 | impbii 208 |
1
β’ (πΉ:π΄βΆπ΅ β βπ₯(πΉ:π΄βontoβπ₯ β§ π₯ β π΅)) |