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	$⊢ F = R freeLMod I$
	frlmrcl.b	$⊢ B = {Base}_{F}$
Assertion	frlmrcl	$⊢ X \in B \to R \in V$

Proof

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