Metamath Proof Explorer

Theorem ovrcl

Description: Reverse closure for an operation value. (Contributed by Mario Carneiro, 5-May-2015)

Ref Expression
Hypothesis ovprc1.1 ⊢ Rel ⁡ dom ⁡ F
Assertion ovrcl ⊢ C ∈ A F B → A ∈ V ∧ B ∈ V

Proof

Step Hyp Ref Expression
1 ovprc1.1 ⊢ Rel ⁡ dom ⁡ F
2 n0i ⊢ C ∈ A F B → ¬ A F B = ∅
3 1 ovprc ⊢ ¬ A ∈ V ∧ B ∈ V → A F B = ∅
4 2 3 nsyl2 ⊢ C ∈ A F B → A ∈ V ∧ B ∈ V