This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
	frlmrcl.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
Assertion	frlmrcl	⊢ ( 𝑋 ∈ 𝐵 → 𝑅 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		frlmval.f	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
2		frlmrcl.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
3		df-frlm	⊢ freeLMod = ( 𝑟 ∈ V , 𝑖 ∈ V ↦ ( 𝑟 ⊕_m ( 𝑖 × { ( ringLMod ‘ 𝑟 ) } ) ) )
4	3	reldmmpo	⊢ Rel dom freeLMod
5	1 2 4	strov2rcl	⊢ ( 𝑋 ∈ 𝐵 → 𝑅 ∈ V )