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

Metamath Proof Explorer

Theorem elfvov2

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

Ref Expression
Hypotheses elfvov1.o ⊢ Rel ⁡ dom ⁡ O
elfvov1.s ⊢ S = I O R
elfvov1.x ⊢ φ → X ∈ S ⁡ Y
Assertion elfvov2 ⊢ φ → R ∈ V

Proof

Step Hyp Ref Expression
1 elfvov1.o ⊢ Rel ⁡ dom ⁡ O
2 elfvov1.s ⊢ S = I O R
3 elfvov1.x ⊢ φ → X ∈ S ⁡ Y
4 n0i ⊢ X ∈ S ⁡ Y → ¬ S ⁡ Y = ∅
5 3 4 syl ⊢ φ → ¬ S ⁡ Y = ∅
6 1 ovprc2 ⊢ ¬ R ∈ V → I O R = ∅
7 2 6 eqtrid ⊢ ¬ R ∈ V → S = ∅
8 7 fveq1d ⊢ ¬ R ∈ V → S ⁡ Y = ∅ ⁡ Y
9 0fv ⊢ ∅ ⁡ Y = ∅
10 8 9 eqtrdi ⊢ ¬ R ∈ V → S ⁡ Y = ∅
11 5 10 nsyl2 ⊢ φ → R ∈ V