Metamath Proof Explorer

Theorem ndmaovrcl

Description: Reverse closure law, in contrast to ndmovrcl where it is required that the operation's domain doesn't contain the empty set ( -. (/) e. S ), no additional asumption is required. (Contributed by Alexander van der Vekens, 26-May-2017)

		Ref	Expression
	Hypothesis	ndmaov.1	$⊢ dom F = S \times S$
	Assertion	ndmaovrcl	$⊢ ((A F B)) \in S \to (A \in S \land B \in S)$

Proof

Step	Hyp	Ref	Expression
1		ndmaov.1	$⊢ dom F = S \times S$
2		aovvdm	$⊢ ((A F B)) \in S \to ⟨A, B⟩ \in dom F$
3		opelxp	$⊢ ⟨A, B⟩ \in (S \times S) \leftrightarrow (A \in S \land B \in S)$
4	3	biimpi	$⊢ ⟨A, B⟩ \in (S \times S) \to (A \in S \land B \in S)$
5	4 1	eleq2s	$⊢ ⟨A, B⟩ \in dom F \to (A \in S \land B \in S)$
6	2 5	syl	$⊢ ((A F B)) \in S \to (A \in S \land B \in S)$