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

Metamath Proof Explorer

Theorem elfvmptrab

Description: Implications for the value of a function defined by the maps-to notation with a class abstraction as a result having an element. (Contributed by Alexander van der Vekens, 15-Jul-2018)

Ref Expression
Hypotheses elfvmptrab.f 
|- F = ( x e. V |-> { y e. M | ph } )
elfvmptrab.v 
|- ( X e. V -> M e. _V )
Assertion elfvmptrab 
|- ( Y e. ( F ` X ) -> ( X e. V /\ Y e. M ) )

Proof

Step Hyp Ref Expression
1 elfvmptrab.f 
 |-  F = ( x e. V |-> { y e. M | ph } )
2 elfvmptrab.v 
 |-  ( X e. V -> M e. _V )
3 csbconstg 
 |-  ( x e. V -> [_ x / m ]_ M = M )
4 3 eqcomd 
 |-  ( x e. V -> M = [_ x / m ]_ M )
5 rabeq 
 |-  ( M = [_ x / m ]_ M -> { y e. M | ph } = { y e. [_ x / m ]_ M | ph } )
6 4 5 syl 
 |-  ( x e. V -> { y e. M | ph } = { y e. [_ x / m ]_ M | ph } )
7 6 mpteq2ia 
 |-  ( x e. V |-> { y e. M | ph } ) = ( x e. V |-> { y e. [_ x / m ]_ M | ph } )
8 1 7 eqtri 
 |-  F = ( x e. V |-> { y e. [_ x / m ]_ M | ph } )
9 csbconstg 
 |-  ( X e. V -> [_ X / m ]_ M = M )
10 9 2 eqeltrd 
 |-  ( X e. V -> [_ X / m ]_ M e. _V )
11 8 10 elfvmptrab1w 
 |-  ( Y e. ( F ` X ) -> ( X e. V /\ Y e. [_ X / m ]_ M ) )
12 9 eleq2d 
 |-  ( X e. V -> ( Y e. [_ X / m ]_ M <-> Y e. M ) )
13 12 biimpd 
 |-  ( X e. V -> ( Y e. [_ X / m ]_ M -> Y e. M ) )
14 13 imdistani 
 |-  ( ( X e. V /\ Y e. [_ X / m ]_ M ) -> ( X e. V /\ Y e. M ) )
15 11 14 syl 
 |-  ( Y e. ( F ` X ) -> ( X e. V /\ Y e. M ) )