Metamath Proof Explorer


Theorem elfvov1

Description: Utility theorem: reverse closure for any operation that results in a function. (Contributed by SN, 18-May-2025)

Ref Expression
Hypotheses elfvov1.o Rel dom O
elfvov1.s S = I O R
elfvov1.x φ X S Y
Assertion elfvov1 φ I V

Proof

Step Hyp Ref Expression
1 elfvov1.o Rel dom O
2 elfvov1.s S = I O R
3 elfvov1.x φ X S Y
4 n0i X S Y ¬ S Y =
5 3 4 syl φ ¬ S Y =
6 1 ovprc1 ¬ I V I O R =
7 2 6 eqtrid ¬ I V S =
8 7 fveq1d ¬ I V S Y = Y
9 0fv Y =
10 8 9 eqtrdi ¬ I V S Y =
11 5 10 nsyl2 φ I V