Step | Hyp | Ref
| Expression |
1 | | simpl2 1193 |
. . . 4
β’ (((π β Univ β§ Fun πΉ β§ (πΉ β π΄) β π) β§ π΄ β π) β Fun πΉ) |
2 | | funrel 6522 |
. . . 4
β’ (Fun
πΉ β Rel πΉ) |
3 | | df-ima 5650 |
. . . . 5
β’ (πΉ β π΄) = ran (πΉ βΎ π΄) |
4 | | resres 5954 |
. . . . . . 7
β’ ((πΉ βΎ dom πΉ) βΎ π΄) = (πΉ βΎ (dom πΉ β© π΄)) |
5 | | resdm 5986 |
. . . . . . . 8
β’ (Rel
πΉ β (πΉ βΎ dom πΉ) = πΉ) |
6 | 5 | reseq1d 5940 |
. . . . . . 7
β’ (Rel
πΉ β ((πΉ βΎ dom πΉ) βΎ π΄) = (πΉ βΎ π΄)) |
7 | 4, 6 | eqtr3id 2787 |
. . . . . 6
β’ (Rel
πΉ β (πΉ βΎ (dom πΉ β© π΄)) = (πΉ βΎ π΄)) |
8 | 7 | rneqd 5897 |
. . . . 5
β’ (Rel
πΉ β ran (πΉ βΎ (dom πΉ β© π΄)) = ran (πΉ βΎ π΄)) |
9 | 3, 8 | eqtr4id 2792 |
. . . 4
β’ (Rel
πΉ β (πΉ β π΄) = ran (πΉ βΎ (dom πΉ β© π΄))) |
10 | 1, 2, 9 | 3syl 18 |
. . 3
β’ (((π β Univ β§ Fun πΉ β§ (πΉ β π΄) β π) β§ π΄ β π) β (πΉ β π΄) = ran (πΉ βΎ (dom πΉ β© π΄))) |
11 | | simpl1 1192 |
. . . 4
β’ (((π β Univ β§ Fun πΉ β§ (πΉ β π΄) β π) β§ π΄ β π) β π β Univ) |
12 | | simpr 486 |
. . . . 5
β’ (((π β Univ β§ Fun πΉ β§ (πΉ β π΄) β π) β§ π΄ β π) β π΄ β π) |
13 | | inss2 4193 |
. . . . . 6
β’ (dom
πΉ β© π΄) β π΄ |
14 | 13 | a1i 11 |
. . . . 5
β’ (((π β Univ β§ Fun πΉ β§ (πΉ β π΄) β π) β§ π΄ β π) β (dom πΉ β© π΄) β π΄) |
15 | | gruss 10740 |
. . . . 5
β’ ((π β Univ β§ π΄ β π β§ (dom πΉ β© π΄) β π΄) β (dom πΉ β© π΄) β π) |
16 | 11, 12, 14, 15 | syl3anc 1372 |
. . . 4
β’ (((π β Univ β§ Fun πΉ β§ (πΉ β π΄) β π) β§ π΄ β π) β (dom πΉ β© π΄) β π) |
17 | | funforn 6767 |
. . . . . . . 8
β’ (Fun
πΉ β πΉ:dom πΉβontoβran πΉ) |
18 | | fof 6760 |
. . . . . . . 8
β’ (πΉ:dom πΉβontoβran πΉ β πΉ:dom πΉβΆran πΉ) |
19 | 17, 18 | sylbi 216 |
. . . . . . 7
β’ (Fun
πΉ β πΉ:dom πΉβΆran πΉ) |
20 | | inss1 4192 |
. . . . . . 7
β’ (dom
πΉ β© π΄) β dom πΉ |
21 | | fssres 6712 |
. . . . . . 7
β’ ((πΉ:dom πΉβΆran πΉ β§ (dom πΉ β© π΄) β dom πΉ) β (πΉ βΎ (dom πΉ β© π΄)):(dom πΉ β© π΄)βΆran πΉ) |
22 | 19, 20, 21 | sylancl 587 |
. . . . . 6
β’ (Fun
πΉ β (πΉ βΎ (dom πΉ β© π΄)):(dom πΉ β© π΄)βΆran πΉ) |
23 | | ffn 6672 |
. . . . . 6
β’ ((πΉ βΎ (dom πΉ β© π΄)):(dom πΉ β© π΄)βΆran πΉ β (πΉ βΎ (dom πΉ β© π΄)) Fn (dom πΉ β© π΄)) |
24 | 1, 22, 23 | 3syl 18 |
. . . . 5
β’ (((π β Univ β§ Fun πΉ β§ (πΉ β π΄) β π) β§ π΄ β π) β (πΉ βΎ (dom πΉ β© π΄)) Fn (dom πΉ β© π΄)) |
25 | | simpl3 1194 |
. . . . . 6
β’ (((π β Univ β§ Fun πΉ β§ (πΉ β π΄) β π) β§ π΄ β π) β (πΉ β π΄) β π) |
26 | 10, 25 | eqsstrrd 3987 |
. . . . 5
β’ (((π β Univ β§ Fun πΉ β§ (πΉ β π΄) β π) β§ π΄ β π) β ran (πΉ βΎ (dom πΉ β© π΄)) β π) |
27 | | df-f 6504 |
. . . . 5
β’ ((πΉ βΎ (dom πΉ β© π΄)):(dom πΉ β© π΄)βΆπ β ((πΉ βΎ (dom πΉ β© π΄)) Fn (dom πΉ β© π΄) β§ ran (πΉ βΎ (dom πΉ β© π΄)) β π)) |
28 | 24, 26, 27 | sylanbrc 584 |
. . . 4
β’ (((π β Univ β§ Fun πΉ β§ (πΉ β π΄) β π) β§ π΄ β π) β (πΉ βΎ (dom πΉ β© π΄)):(dom πΉ β© π΄)βΆπ) |
29 | | grurn 10745 |
. . . 4
β’ ((π β Univ β§ (dom πΉ β© π΄) β π β§ (πΉ βΎ (dom πΉ β© π΄)):(dom πΉ β© π΄)βΆπ) β ran (πΉ βΎ (dom πΉ β© π΄)) β π) |
30 | 11, 16, 28, 29 | syl3anc 1372 |
. . 3
β’ (((π β Univ β§ Fun πΉ β§ (πΉ β π΄) β π) β§ π΄ β π) β ran (πΉ βΎ (dom πΉ β© π΄)) β π) |
31 | 10, 30 | eqeltrd 2834 |
. 2
β’ (((π β Univ β§ Fun πΉ β§ (πΉ β π΄) β π) β§ π΄ β π) β (πΉ β π΄) β π) |
32 | 31 | ex 414 |
1
β’ ((π β Univ β§ Fun πΉ β§ (πΉ β π΄) β π) β (π΄ β π β (πΉ β π΄) β π)) |