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

Metamath Proof Explorer

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	⊢ 𝑆 = ( 𝐼 𝐹 𝑅 )
	strov2rcl.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	strov2rcl.f	⊢ Rel dom 𝐹
Assertion	strov2rcl	⊢ ( 𝑋 ∈ 𝐵 → 𝐼 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		strov2rcl.s	⊢ 𝑆 = ( 𝐼 𝐹 𝑅 )
2		strov2rcl.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
3		strov2rcl.f	⊢ Rel dom 𝐹
4	3 1 2	elbasov	⊢ ( 𝑋 ∈ 𝐵 → ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) )
5	4	simpld	⊢ ( 𝑋 ∈ 𝐵 → 𝐼 ∈ V )