Theorem ovrcl

Description: Reverse closure for an operation value. (Contributed by Mario Carneiro, 5-May-2015)

	Ref	Expression
Hypothesis	ovprc1.1	$$⊢\mathrm{Rel}\mathrm{dom}F$$
Assertion	ovrcl	$$⊢C\in \left(AFB\right)\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$

Proof

Step	Hyp	Ref	Expression
1		ovprc1.1	$$⊢\mathrm{Rel}\mathrm{dom}F$$
2		n0i	$$⊢C\in \left(AFB\right)\to \neg AFB=\varnothing$$
3	1	ovprc	$$⊢\neg \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to AFB=\varnothing$$
4	2 3	nsyl2	$$⊢C\in \left(AFB\right)\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$