Metamath Proof Explorer


Theorem elbasov

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 ReldomO
elbasov.s S=XOY
elbasov.b B=BaseS
Assertion elbasov ABXVYV

Proof

Step Hyp Ref Expression
1 elbasov.o ReldomO
2 elbasov.s S=XOY
3 elbasov.b B=BaseS
4 n0i AB¬B=
5 1 ovprc ¬XVYVXOY=
6 2 5 eqtrid ¬XVYVS=
7 6 fveq2d ¬XVYVBaseS=Base
8 base0 =Base
9 7 3 8 3eqtr4g ¬XVYVB=
10 4 9 nsyl2 ABXVYV