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	$$⊢\mathrm{Rel}\mathrm{dom}O$$
	elfvov1.s	$$⊢S=IOR$$
	elfvov1.x	$$⊢\phi \to X\in S\left(Y\right)$$
Assertion	elfvov1	$$⊢\phi \to I\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		elfvov1.o	$$⊢\mathrm{Rel}\mathrm{dom}O$$
2		elfvov1.s	$$⊢S=IOR$$
3		elfvov1.x	$$⊢\phi \to X\in S\left(Y\right)$$
4		n0i	$$⊢X\in S\left(Y\right)\to \neg S\left(Y\right)=\varnothing$$
5	3 4	syl	$$⊢\phi \to \neg S\left(Y\right)=\varnothing$$
6	1	ovprc1	$$⊢\neg I\in \mathrm{V}\to IOR=\varnothing$$
7	2 6	eqtrid	$$⊢\neg I\in \mathrm{V}\to S=\varnothing$$
8	7	fveq1d	$$⊢\neg I\in \mathrm{V}\to S\left(Y\right)=\varnothing \left(Y\right)$$
9		0fv	$$⊢\varnothing \left(Y\right)=\varnothing$$
10	8 9	eqtrdi	$$⊢\neg I\in \mathrm{V}\to S\left(Y\right)=\varnothing$$
11	5 10	nsyl2	$$⊢\phi \to I\in \mathrm{V}$$