Step | Hyp | Ref
| Expression |
1 | | setpreimafvex.p |
. . . . 5
β’ π = {π§ β£ βπ₯ β π΄ π§ = (β‘πΉ β {(πΉβπ₯)})} |
2 | 1 | 0nelsetpreimafv 45672 |
. . . 4
β’ (πΉ Fn π΄ β β
β π) |
3 | | elnelne2 3057 |
. . . . . 6
β’ ((π β π β§ β
β π) β π β β
) |
4 | | n0 4310 |
. . . . . 6
β’ (π β β
β
βπ¦ π¦ β π) |
5 | 3, 4 | sylib 217 |
. . . . 5
β’ ((π β π β§ β
β π) β βπ¦ π¦ β π) |
6 | 5 | expcom 415 |
. . . 4
β’ (β
β π β (π β π β βπ¦ π¦ β π)) |
7 | 2, 6 | syl 17 |
. . 3
β’ (πΉ Fn π΄ β (π β π β βπ¦ π¦ β π)) |
8 | 7 | imp 408 |
. 2
β’ ((πΉ Fn π΄ β§ π β π) β βπ¦ π¦ β π) |
9 | 1 | imaelsetpreimafv 45677 |
. . . . . 6
β’ ((πΉ Fn π΄ β§ π β π β§ π¦ β π) β (πΉ β π) = {(πΉβπ¦)}) |
10 | 9 | 3expa 1119 |
. . . . 5
β’ (((πΉ Fn π΄ β§ π β π) β§ π¦ β π) β (πΉ β π) = {(πΉβπ¦)}) |
11 | 10 | unieqd 4883 |
. . . 4
β’ (((πΉ Fn π΄ β§ π β π) β§ π¦ β π) β βͺ (πΉ β π) = βͺ {(πΉβπ¦)}) |
12 | | fvex 6859 |
. . . . 5
β’ (πΉβπ¦) β V |
13 | 12 | unisn 4891 |
. . . 4
β’ βͺ {(πΉβπ¦)} = (πΉβπ¦) |
14 | 11, 13 | eqtrdi 2789 |
. . 3
β’ (((πΉ Fn π΄ β§ π β π) β§ π¦ β π) β βͺ (πΉ β π) = (πΉβπ¦)) |
15 | | dffn3 6685 |
. . . . . 6
β’ (πΉ Fn π΄ β πΉ:π΄βΆran πΉ) |
16 | 15 | biimpi 215 |
. . . . 5
β’ (πΉ Fn π΄ β πΉ:π΄βΆran πΉ) |
17 | 16 | ad2antrr 725 |
. . . 4
β’ (((πΉ Fn π΄ β§ π β π) β§ π¦ β π) β πΉ:π΄βΆran πΉ) |
18 | 1 | elsetpreimafvssdm 45668 |
. . . . 5
β’ ((πΉ Fn π΄ β§ π β π) β π β π΄) |
19 | 18 | sselda 3948 |
. . . 4
β’ (((πΉ Fn π΄ β§ π β π) β§ π¦ β π) β π¦ β π΄) |
20 | 17, 19 | ffvelcdmd 7040 |
. . 3
β’ (((πΉ Fn π΄ β§ π β π) β§ π¦ β π) β (πΉβπ¦) β ran πΉ) |
21 | 14, 20 | eqeltrd 2834 |
. 2
β’ (((πΉ Fn π΄ β§ π β π) β§ π¦ β π) β βͺ (πΉ β π) β ran πΉ) |
22 | 8, 21 | exlimddv 1939 |
1
β’ ((πΉ Fn π΄ β§ π β π) β βͺ (πΉ β π) β ran πΉ) |