Description: Reverse closure for an arrow. (Contributed by Mario Carneiro, 11-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypothesis | homarcl.h | ||
Assertion | homarcl |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | homarcl.h | ||
2 | n0i | ||
3 | df-homa | ||
4 | 3 | fvmptndm | |
5 | 1 4 | eqtrid | |
6 | 5 | oveqd | |
7 | 0ov | ||
8 | 6 7 | eqtrdi | |
9 | 2 8 | nsyl2 |