Step | Hyp | Ref
| Expression |
1 | | df-ima 5690 |
. 2
β’ (πΉ β π΄) = ran (πΉ βΎ π΄) |
2 | | funres 6591 |
. . . . . . . 8
β’ (Fun
πΉ β Fun (πΉ βΎ π΄)) |
3 | | funforn 6813 |
. . . . . . . 8
β’ (Fun
(πΉ βΎ π΄) β (πΉ βΎ π΄):dom (πΉ βΎ π΄)βontoβran (πΉ βΎ π΄)) |
4 | 2, 3 | sylib 217 |
. . . . . . 7
β’ (Fun
πΉ β (πΉ βΎ π΄):dom (πΉ βΎ π΄)βontoβran (πΉ βΎ π΄)) |
5 | 4 | 3ad2ant1 1134 |
. . . . . 6
β’ ((Fun
πΉ β§ π΄ β π β§ (πΉ β π΄) β π) β (πΉ βΎ π΄):dom (πΉ βΎ π΄)βontoβran (πΉ βΎ π΄)) |
6 | | fof 6806 |
. . . . . 6
β’ ((πΉ βΎ π΄):dom (πΉ βΎ π΄)βontoβran (πΉ βΎ π΄) β (πΉ βΎ π΄):dom (πΉ βΎ π΄)βΆran (πΉ βΎ π΄)) |
7 | 5, 6 | syl 17 |
. . . . 5
β’ ((Fun
πΉ β§ π΄ β π β§ (πΉ β π΄) β π) β (πΉ βΎ π΄):dom (πΉ βΎ π΄)βΆran (πΉ βΎ π΄)) |
8 | | dmres 6004 |
. . . . . . 7
β’ dom
(πΉ βΎ π΄) = (π΄ β© dom πΉ) |
9 | | inss1 4229 |
. . . . . . 7
β’ (π΄ β© dom πΉ) β π΄ |
10 | 8, 9 | eqsstri 4017 |
. . . . . 6
β’ dom
(πΉ βΎ π΄) β π΄ |
11 | | simp2 1138 |
. . . . . 6
β’ ((Fun
πΉ β§ π΄ β π β§ (πΉ β π΄) β π) β π΄ β π) |
12 | | ssexg 5324 |
. . . . . 6
β’ ((dom
(πΉ βΎ π΄) β π΄ β§ π΄ β π) β dom (πΉ βΎ π΄) β V) |
13 | 10, 11, 12 | sylancr 588 |
. . . . 5
β’ ((Fun
πΉ β§ π΄ β π β§ (πΉ β π΄) β π) β dom (πΉ βΎ π΄) β V) |
14 | | simp3 1139 |
. . . . . 6
β’ ((Fun
πΉ β§ π΄ β π β§ (πΉ β π΄) β π) β (πΉ β π΄) β π) |
15 | 1, 14 | eqeltrrid 2839 |
. . . . 5
β’ ((Fun
πΉ β§ π΄ β π β§ (πΉ β π΄) β π) β ran (πΉ βΎ π΄) β π) |
16 | | fex2 7924 |
. . . . 5
β’ (((πΉ βΎ π΄):dom (πΉ βΎ π΄)βΆran (πΉ βΎ π΄) β§ dom (πΉ βΎ π΄) β V β§ ran (πΉ βΎ π΄) β π) β (πΉ βΎ π΄) β V) |
17 | 7, 13, 15, 16 | syl3anc 1372 |
. . . 4
β’ ((Fun
πΉ β§ π΄ β π β§ (πΉ β π΄) β π) β (πΉ βΎ π΄) β V) |
18 | | fowdom 9566 |
. . . 4
β’ (((πΉ βΎ π΄) β V β§ (πΉ βΎ π΄):dom (πΉ βΎ π΄)βontoβran (πΉ βΎ π΄)) β ran (πΉ βΎ π΄) βΌ* dom (πΉ βΎ π΄)) |
19 | 17, 5, 18 | syl2anc 585 |
. . 3
β’ ((Fun
πΉ β§ π΄ β π β§ (πΉ β π΄) β π) β ran (πΉ βΎ π΄) βΌ* dom (πΉ βΎ π΄)) |
20 | | ssdomg 8996 |
. . . . . 6
β’ (π΄ β π β (dom (πΉ βΎ π΄) β π΄ β dom (πΉ βΎ π΄) βΌ π΄)) |
21 | 10, 20 | mpi 20 |
. . . . 5
β’ (π΄ β π β dom (πΉ βΎ π΄) βΌ π΄) |
22 | | domwdom 9569 |
. . . . 5
β’ (dom
(πΉ βΎ π΄) βΌ π΄ β dom (πΉ βΎ π΄) βΌ* π΄) |
23 | 21, 22 | syl 17 |
. . . 4
β’ (π΄ β π β dom (πΉ βΎ π΄) βΌ* π΄) |
24 | 23 | 3ad2ant2 1135 |
. . 3
β’ ((Fun
πΉ β§ π΄ β π β§ (πΉ β π΄) β π) β dom (πΉ βΎ π΄) βΌ* π΄) |
25 | | wdomtr 9570 |
. . 3
β’ ((ran
(πΉ βΎ π΄) βΌ* dom (πΉ βΎ π΄) β§ dom (πΉ βΎ π΄) βΌ* π΄) β ran (πΉ βΎ π΄) βΌ* π΄) |
26 | 19, 24, 25 | syl2anc 585 |
. 2
β’ ((Fun
πΉ β§ π΄ β π β§ (πΉ β π΄) β π) β ran (πΉ βΎ π΄) βΌ* π΄) |
27 | 1, 26 | eqbrtrid 5184 |
1
β’ ((Fun
πΉ β§ π΄ β π β§ (πΉ β π΄) β π) β (πΉ β π΄) βΌ* π΄) |