Theorem frlmrcl

Description: If a free module is inhabited, this is sufficient to conclude that the ring expression defines a set. (Contributed by Stefan O'Rear, 3-Feb-2015)

	Ref	Expression
Hypotheses	frlmval.f	$$⊢F=R\mathrm{freeLMod}I$$
	frlmrcl.b	$$⊢B={\mathrm{Base}}_F$$
Assertion	frlmrcl	$$⊢X\in B\to R\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		frlmval.f	$$⊢F=R\mathrm{freeLMod}I$$
2		frlmrcl.b	$$⊢B={\mathrm{Base}}_F$$
3		df-frlm	$$⊢\mathrm{freeLMod}=\left(r\in \mathrm{V},i\in \mathrm{V}⟼r{\oplus }_m\left(i\times \left\{\mathrm{ringLMod}\left(r\right)\right\}\right)\right)$$
4	3	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{freeLMod}$$
5	1 2 4	strov2rcl	$$⊢X\in B\to R\in \mathrm{V}$$