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)) \in C \to (A \in V \land B \in 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)) \in C \leftrightarrow (F''' ⟨A, B⟩) \in C$
4		afvvdm	$⊢ (F''' ⟨A, B⟩) \in C \to ⟨A, B⟩ \in dom F$
5		df-br	$⊢ A dom F B \leftrightarrow ⟨A, B⟩ \in dom F$
6	1	brrelex12i	$⊢ A dom F B \to (A \in V \land B \in V)$
7	5 6	sylbir	$⊢ ⟨A, B⟩ \in dom F \to (A \in V \land B \in V)$
8	4 7	syl	$⊢ (F''' ⟨A, B⟩) \in C \to (A \in V \land B \in V)$
9	3 8	sylbi	$⊢ ((A F B)) \in C \to (A \in V \land B \in V)$

Metamath Proof Explorer

Theorem aovrcl

Proof