elrnmpoid

Description: Membership in the range of an operation class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021)

		Ref	Expression
	Hypothesis	elrnmpoid.1	$⊢ F = (x \in A, y \in B ⟼ C)$
	Assertion	elrnmpoid	$⊢ (x \in A \land y \in B \land \forall x \in A \forall y \in B C \in V) \to x F y \in ran F$

Step	Hyp	Ref	Expression
1		elrnmpoid.1	$⊢ F = (x \in A, y \in B ⟼ C)$
2	1	fnmpo	$⊢ \forall x \in A \forall y \in B C \in V \to F Fn (A \times B)$
3	2	3ad2ant3	$⊢ (x \in A \land y \in B \land \forall x \in A \forall y \in B C \in V) \to F Fn (A \times B)$
4		simp1	$⊢ (x \in A \land y \in B \land \forall x \in A \forall y \in B C \in V) \to x \in A$
5		simp2	$⊢ (x \in A \land y \in B \land \forall x \in A \forall y \in B C \in V) \to y \in B$
6		fnovrn	$⊢ (F Fn (A \times B) \land x \in A \land y \in B) \to x F y \in ran F$
7	3 4 5 6	syl3anc	$⊢ (x \in A \land y \in B \land \forall x \in A \forall y \in B C \in V) \to x F y \in ran F$

Metamath Proof Explorer