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	$$⊢\mathrm{Rel}\mathrm{dom}O$$
	elbasov.s	$$⊢S=XOY$$
	elbasov.b	$$⊢B={\mathrm{Base}}_S$$
Assertion	elbasov	$$⊢A\in B\to \left(X\in \mathrm{V}\wedge Y\in \mathrm{V}\right)$$

Proof

Step	Hyp	Ref	Expression
1		elbasov.o	$$⊢\mathrm{Rel}\mathrm{dom}O$$
2		elbasov.s	$$⊢S=XOY$$
3		elbasov.b	$$⊢B={\mathrm{Base}}_S$$
4		n0i	$$⊢A\in B\to \neg B=\varnothing$$
5	1	ovprc	$$⊢\neg \left(X\in \mathrm{V}\wedge Y\in \mathrm{V}\right)\to XOY=\varnothing$$
6	2 5	syl5eq	$$⊢\neg \left(X\in \mathrm{V}\wedge Y\in \mathrm{V}\right)\to S=\varnothing$$
7	6	fveq2d	$$⊢\neg \left(X\in \mathrm{V}\wedge Y\in \mathrm{V}\right)\to {\mathrm{Base}}_S={\mathrm{Base}}_{\varnothing }$$
8		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
9	7 3 8	3eqtr4g	$$⊢\neg \left(X\in \mathrm{V}\wedge Y\in \mathrm{V}\right)\to B=\varnothing$$
10	4 9	nsyl2	$$⊢A\in B\to \left(X\in \mathrm{V}\wedge Y\in \mathrm{V}\right)$$