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 Rel dom O
elbasov.s S = X O Y
elbasov.b B = Base S
Assertion elbasov A B X V Y V

Proof

Step Hyp Ref Expression
1 elbasov.o Rel dom O
2 elbasov.s S = X O Y
3 elbasov.b B = Base S
4 n0i A B ¬ B =
5 1 ovprc ¬ X V Y V X O Y =
6 2 5 syl5eq ¬ X V Y V S =
7 6 fveq2d ¬ X V Y V Base S = Base
8 base0 = Base
9 7 3 8 3eqtr4g ¬ X V Y V B =
10 4 9 nsyl2 A B X V Y V