Theorem elbasfv

Description: Utility theorem: reverse closure for any structure defined as a function. (Contributed by Stefan O'Rear, 24-Aug-2015)

	Ref	Expression
Hypotheses	elbasfv.s	$$⊢S=F\left(Z\right)$$
	elbasfv.b	$$⊢B={\mathrm{Base}}_S$$
Assertion	elbasfv	$$⊢X\in B\to Z\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		elbasfv.s	$$⊢S=F\left(Z\right)$$
2		elbasfv.b	$$⊢B={\mathrm{Base}}_S$$
3		n0i	$$⊢X\in B\to \neg B=\varnothing$$
4		fvprc	$$⊢\neg Z\in \mathrm{V}\to F\left(Z\right)=\varnothing$$
5	1 4	eqtrid	$$⊢\neg Z\in \mathrm{V}\to S=\varnothing$$
6	5	fveq2d	$$⊢\neg Z\in \mathrm{V}\to {\mathrm{Base}}_S={\mathrm{Base}}_{\varnothing }$$
7		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
8	6 2 7	3eqtr4g	$$⊢\neg Z\in \mathrm{V}\to B=\varnothing$$
9	3 8	nsyl2	$$⊢X\in B\to Z\in \mathrm{V}$$