Theorem strov2rcl

Description: Partial reverse closure for any structure defined as a two-argument function. (Contributed by Stefan O'Rear, 27-Mar-2015) (Proof shortened by AV, 2-Dec-2019)

	Ref	Expression
Hypotheses	strov2rcl.s	$$⊢S=IFR$$
	strov2rcl.b	$$⊢B={\mathrm{Base}}_S$$
	strov2rcl.f	$$⊢\mathrm{Rel}\mathrm{dom}F$$
Assertion	strov2rcl	$$⊢X\in B\to I\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		strov2rcl.s	$$⊢S=IFR$$
2		strov2rcl.b	$$⊢B={\mathrm{Base}}_S$$
3		strov2rcl.f	$$⊢\mathrm{Rel}\mathrm{dom}F$$
4	3 1 2	elbasov	$$⊢X\in B\to \left(I\in \mathrm{V}\wedge R\in \mathrm{V}\right)$$
5	4	simpld	$$⊢X\in B\to I\in \mathrm{V}$$