Description: Utility theorem: reverse closure for any structure defined as a two-argument function. (Contributed by Mario Carneiro, 3-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | elbasov.o | ||
elbasov.s | |||
elbasov.b | |||
Assertion | elbasov |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elbasov.o | ||
2 | elbasov.s | ||
3 | elbasov.b | ||
4 | n0i | ||
5 | 1 | ovprc | |
6 | 2 5 | syl5eq | |
7 | 6 | fveq2d | |
8 | base0 | ||
9 | 7 3 8 | 3eqtr4g | |
10 | 4 9 | nsyl2 |