Step | Hyp | Ref
| Expression |
1 | | relco 6061 |
. . 3
β’ Rel
(β‘πΉ β πΉ) |
2 | 1 | a1i 11 |
. 2
β’ (πΉ Fn π β Rel (β‘πΉ β πΉ)) |
3 | | dmco 6207 |
. . 3
β’ dom
(β‘πΉ β πΉ) = (β‘πΉ β dom β‘πΉ) |
4 | | df-rn 5645 |
. . . . 5
β’ ran πΉ = dom β‘πΉ |
5 | 4 | imaeq2i 6012 |
. . . 4
β’ (β‘πΉ β ran πΉ) = (β‘πΉ β dom β‘πΉ) |
6 | | cnvimarndm 6035 |
. . . . 5
β’ (β‘πΉ β ran πΉ) = dom πΉ |
7 | | fndm 6606 |
. . . . 5
β’ (πΉ Fn π β dom πΉ = π) |
8 | 6, 7 | eqtrid 2789 |
. . . 4
β’ (πΉ Fn π β (β‘πΉ β ran πΉ) = π) |
9 | 5, 8 | eqtr3id 2791 |
. . 3
β’ (πΉ Fn π β (β‘πΉ β dom β‘πΉ) = π) |
10 | 3, 9 | eqtrid 2789 |
. 2
β’ (πΉ Fn π β dom (β‘πΉ β πΉ) = π) |
11 | | cnvco 5842 |
. . . . 5
β’ β‘(β‘πΉ β πΉ) = (β‘πΉ β β‘β‘πΉ) |
12 | | cnvcnvss 6147 |
. . . . . 6
β’ β‘β‘πΉ β πΉ |
13 | | coss2 5813 |
. . . . . 6
β’ (β‘β‘πΉ β πΉ β (β‘πΉ β β‘β‘πΉ) β (β‘πΉ β πΉ)) |
14 | 12, 13 | ax-mp 5 |
. . . . 5
β’ (β‘πΉ β β‘β‘πΉ) β (β‘πΉ β πΉ) |
15 | 11, 14 | eqsstri 3979 |
. . . 4
β’ β‘(β‘πΉ β πΉ) β (β‘πΉ β πΉ) |
16 | 15 | a1i 11 |
. . 3
β’ (πΉ Fn π β β‘(β‘πΉ β πΉ) β (β‘πΉ β πΉ)) |
17 | | coass 6218 |
. . . . 5
β’ ((β‘πΉ β πΉ) β (β‘πΉ β πΉ)) = (β‘πΉ β (πΉ β (β‘πΉ β πΉ))) |
18 | | coass 6218 |
. . . . . . 7
β’ ((πΉ β β‘πΉ) β πΉ) = (πΉ β (β‘πΉ β πΉ)) |
19 | | fnfun 6603 |
. . . . . . . . . 10
β’ (πΉ Fn π β Fun πΉ) |
20 | | funcocnv2 6810 |
. . . . . . . . . 10
β’ (Fun
πΉ β (πΉ β β‘πΉ) = ( I βΎ ran πΉ)) |
21 | 19, 20 | syl 17 |
. . . . . . . . 9
β’ (πΉ Fn π β (πΉ β β‘πΉ) = ( I βΎ ran πΉ)) |
22 | 21 | coeq1d 5818 |
. . . . . . . 8
β’ (πΉ Fn π β ((πΉ β β‘πΉ) β πΉ) = (( I βΎ ran πΉ) β πΉ)) |
23 | | dffn3 6682 |
. . . . . . . . 9
β’ (πΉ Fn π β πΉ:πβΆran πΉ) |
24 | | fcoi2 6718 |
. . . . . . . . 9
β’ (πΉ:πβΆran πΉ β (( I βΎ ran πΉ) β πΉ) = πΉ) |
25 | 23, 24 | sylbi 216 |
. . . . . . . 8
β’ (πΉ Fn π β (( I βΎ ran πΉ) β πΉ) = πΉ) |
26 | 22, 25 | eqtrd 2777 |
. . . . . . 7
β’ (πΉ Fn π β ((πΉ β β‘πΉ) β πΉ) = πΉ) |
27 | 18, 26 | eqtr3id 2791 |
. . . . . 6
β’ (πΉ Fn π β (πΉ β (β‘πΉ β πΉ)) = πΉ) |
28 | 27 | coeq2d 5819 |
. . . . 5
β’ (πΉ Fn π β (β‘πΉ β (πΉ β (β‘πΉ β πΉ))) = (β‘πΉ β πΉ)) |
29 | 17, 28 | eqtrid 2789 |
. . . 4
β’ (πΉ Fn π β ((β‘πΉ β πΉ) β (β‘πΉ β πΉ)) = (β‘πΉ β πΉ)) |
30 | | ssid 3967 |
. . . 4
β’ (β‘πΉ β πΉ) β (β‘πΉ β πΉ) |
31 | 29, 30 | eqsstrdi 3999 |
. . 3
β’ (πΉ Fn π β ((β‘πΉ β πΉ) β (β‘πΉ β πΉ)) β (β‘πΉ β πΉ)) |
32 | 16, 31 | unssd 4147 |
. 2
β’ (πΉ Fn π β (β‘(β‘πΉ β πΉ) βͺ ((β‘πΉ β πΉ) β (β‘πΉ β πΉ))) β (β‘πΉ β πΉ)) |
33 | | df-er 8649 |
. 2
β’ ((β‘πΉ β πΉ) Er π β (Rel (β‘πΉ β πΉ) β§ dom (β‘πΉ β πΉ) = π β§ (β‘(β‘πΉ β πΉ) βͺ ((β‘πΉ β πΉ) β (β‘πΉ β πΉ))) β (β‘πΉ β πΉ))) |
34 | 2, 10, 32, 33 | syl3anbrc 1344 |
1
β’ (πΉ Fn π β (β‘πΉ β πΉ) Er π) |