This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 e. A , y e. B |-> C )
Assertion elrnmpoid 
|- ( ( x e. A /\ y e. B /\ A. x e. A A. y e. B C e. V ) -> ( x F y ) e. ran F )

Proof

Step Hyp Ref Expression
1 elrnmpoid.1 
 |-  F = ( x e. A , y e. B |-> C )
2 1 fnmpo 
 |-  ( A. x e. A A. y e. B C e. V -> F Fn ( A X. B ) )
3 2 3ad2ant3 
 |-  ( ( x e. A /\ y e. B /\ A. x e. A A. y e. B C e. V ) -> F Fn ( A X. B ) )
4 simp1 
 |-  ( ( x e. A /\ y e. B /\ A. x e. A A. y e. B C e. V ) -> x e. A )
5 simp2 
 |-  ( ( x e. A /\ y e. B /\ A. x e. A A. y e. B C e. V ) -> y e. B )
6 fnovrn 
 |-  ( ( F Fn ( A X. B ) /\ x e. A /\ y e. B ) -> ( x F y ) e. ran F )
7 3 4 5 6 syl3anc 
 |-  ( ( x e. A /\ y e. B /\ A. x e. A A. y e. B C e. V ) -> ( x F y ) e. ran F )