Theorem elfvov1

Description: Utility theorem: reverse closure for any operation that results in a function. (Contributed by SN, 18-May-2025)

	Ref	Expression
Hypotheses	elfvov1.o	⊢ Rel dom 𝑂
	elfvov1.s	⊢ 𝑆 = ( 𝐼 𝑂 𝑅 )
	elfvov1.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑆 ‘ 𝑌 ) )
Assertion	elfvov1	⊢ ( 𝜑 → 𝐼 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		elfvov1.o	⊢ Rel dom 𝑂
2		elfvov1.s	⊢ 𝑆 = ( 𝐼 𝑂 𝑅 )
3		elfvov1.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑆 ‘ 𝑌 ) )
4		n0i	⊢ ( 𝑋 ∈ ( 𝑆 ‘ 𝑌 ) → ¬ ( 𝑆 ‘ 𝑌 ) = ∅ )
5	3 4	syl	⊢ ( 𝜑 → ¬ ( 𝑆 ‘ 𝑌 ) = ∅ )
6	1	ovprc1	⊢ ( ¬ 𝐼 ∈ V → ( 𝐼 𝑂 𝑅 ) = ∅ )
7	2 6	eqtrid	⊢ ( ¬ 𝐼 ∈ V → 𝑆 = ∅ )
8	7	fveq1d	⊢ ( ¬ 𝐼 ∈ V → ( 𝑆 ‘ 𝑌 ) = ( ∅ ‘ 𝑌 ) )
9		0fv	⊢ ( ∅ ‘ 𝑌 ) = ∅
10	8 9	eqtrdi	⊢ ( ¬ 𝐼 ∈ V → ( 𝑆 ‘ 𝑌 ) = ∅ )
11	5 10	nsyl2	⊢ ( 𝜑 → 𝐼 ∈ V )