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 freeLMod I )
	frlmrcl.b	|- B = ( Base ` F )
Assertion	frlmrcl	|- ( X e. B -> R e. _V )

Proof

Step	Hyp	Ref	Expression
1		frlmval.f	|- F = ( R freeLMod I )
2		frlmrcl.b	|- B = ( Base ` F )
3		df-frlm	|- freeLMod = ( r e. _V , i e. _V |-> ( r (+)m ( i X. { ( ringLMod ` r ) } ) ) )
4	3	reldmmpo	|- Rel dom freeLMod
5	1 2 4	strov2rcl	|- ( X e. B -> R e. _V )