Metamath Proof Explorer

Theorem aovrcl

Description: Reverse closure for an operation value, analogous to afvvv . In contrast to ovrcl , elementhood of the operation's value in a set is required, not containing an element. (Contributed by Alexander van der Vekens, 26-May-2017)

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

Proof

Step Hyp Ref Expression
1 aovprc.1 ⊢ Rel ⁡ dom ⁡ F
2 df-aov ⊢ A F B = F ''' A B
3 2 eleq1i ⊢ A F B ∈ C ↔ F ''' A B ∈ C
4 afvvdm ⊢ F ''' A B ∈ C → A B ∈ dom ⁡ F
5 df-br ⊢ A dom ⁡ F B ↔ A B ∈ dom ⁡ F
6 1 brrelex12i ⊢ A dom ⁡ F B → A ∈ V ∧ B ∈ V
7 5 6 sylbir ⊢ A B ∈ dom ⁡ F → A ∈ V ∧ B ∈ V
8 4 7 syl ⊢ F ''' A B ∈ C → A ∈ V ∧ B ∈ V
9 3 8 sylbi ⊢ A F B ∈ C → A ∈ V ∧ B ∈ V