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 | eqtrid | |
7 | 6 | fveq2d | |
8 | base0 | |
|
9 | 7 3 8 | 3eqtr4g | |
10 | 4 9 | nsyl2 | |