Step | Hyp | Ref
| Expression |
1 | | elex 3465 |
. . . 4
β’ (πΉ β π΄ β πΉ β V) |
2 | | gneispace.a |
. . . . 5
β’ π΄ = {π β£ (π:dom πβΆ(π« (π« dom π β {β
}) β
{β
}) β§ βπ
β dom πβπ β (πβπ)(π β π β§ βπ β π« dom π(π β π β π β (πβπ))))} |
3 | 2 | gneispace 42498 |
. . . 4
β’ (πΉ β V β (πΉ β π΄ β (Fun πΉ β§ ran πΉ β π« π« dom πΉ β§ βπ β dom πΉ((πΉβπ) β β
β§ βπ β (πΉβπ)(π β π β§ βπ β π« dom πΉ(π β π β π β (πΉβπ))))))) |
4 | 1, 3 | syl 17 |
. . 3
β’ (πΉ β π΄ β (πΉ β π΄ β (Fun πΉ β§ ran πΉ β π« π« dom πΉ β§ βπ β dom πΉ((πΉβπ) β β
β§ βπ β (πΉβπ)(π β π β§ βπ β π« dom πΉ(π β π β π β (πΉβπ))))))) |
5 | 4 | ibi 267 |
. 2
β’ (πΉ β π΄ β (Fun πΉ β§ ran πΉ β π« π« dom πΉ β§ βπ β dom πΉ((πΉβπ) β β
β§ βπ β (πΉβπ)(π β π β§ βπ β π« dom πΉ(π β π β π β (πΉβπ)))))) |
6 | | simp1 1137 |
. . . 4
β’ ((Fun
πΉ β§ ran πΉ β π« π« dom
πΉ β§ βπ β dom πΉ((πΉβπ) β β
β§ βπ β (πΉβπ)(π β π β§ βπ β π« dom πΉ(π β π β π β (πΉβπ))))) β Fun πΉ) |
7 | 6 | funfnd 6536 |
. . 3
β’ ((Fun
πΉ β§ ran πΉ β π« π« dom
πΉ β§ βπ β dom πΉ((πΉβπ) β β
β§ βπ β (πΉβπ)(π β π β§ βπ β π« dom πΉ(π β π β π β (πΉβπ))))) β πΉ Fn dom πΉ) |
8 | | simp2 1138 |
. . 3
β’ ((Fun
πΉ β§ ran πΉ β π« π« dom
πΉ β§ βπ β dom πΉ((πΉβπ) β β
β§ βπ β (πΉβπ)(π β π β§ βπ β π« dom πΉ(π β π β π β (πΉβπ))))) β ran πΉ β π« π« dom πΉ) |
9 | | df-f 6504 |
. . 3
β’ (πΉ:dom πΉβΆπ« π« dom πΉ β (πΉ Fn dom πΉ β§ ran πΉ β π« π« dom πΉ)) |
10 | 7, 8, 9 | sylanbrc 584 |
. 2
β’ ((Fun
πΉ β§ ran πΉ β π« π« dom
πΉ β§ βπ β dom πΉ((πΉβπ) β β
β§ βπ β (πΉβπ)(π β π β§ βπ β π« dom πΉ(π β π β π β (πΉβπ))))) β πΉ:dom πΉβΆπ« π« dom πΉ) |
11 | 5, 10 | syl 17 |
1
β’ (πΉ β π΄ β πΉ:dom πΉβΆπ« π« dom πΉ) |