Metamath Proof Explorer

Theorem elfvmptrab1w

Description: Implications for the value of a function defined by the maps-to notation with a class abstraction as a result having an element. Here, the base set of the class abstraction depends on the argument of the function. Version of elfvmptrab1 with a disjoint variable condition, which does not require ax-13 . (Contributed by Alexander van der Vekens, 15-Jul-2018) (Revised by Gino Giotto, 26-Jan-2024)

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

Proof

Step Hyp Ref Expression
1 elfvmptrab1w.f 
 |-  F = ( x e. V |-> { y e. [_ x / m ]_ M | ph } )
2 elfvmptrab1w.v 
 |-  ( X e. V -> [_ X / m ]_ M e. _V )
3 elfvdm 
 |-  ( Y e. ( F ` X ) -> X e. dom F )
4 1 dmmptss 
 |-  dom F C_ V
5 4 sseli 
 |-  ( X e. dom F -> X e. V )
6 rabexg 
 |-  ( [_ X / m ]_ M e. _V -> { y e. [_ X / m ]_ M | [. X / x ]. ph } e. _V )
7 5 2 6 3syl 
 |-  ( X e. dom F -> { y e. [_ X / m ]_ M | [. X / x ]. ph } e. _V )
8 nfcv 
 |-  F/_ x X
9 nfsbc1v 
 |-  F/ x [. X / x ]. ph
10 nfcv 
 |-  F/_ x M
11 8 10 nfcsbw 
 |-  F/_ x [_ X / m ]_ M
12 9 11 nfrabw 
 |-  F/_ x { y e. [_ X / m ]_ M | [. X / x ]. ph }
13 csbeq1 
 |-  ( x = X -> [_ x / m ]_ M = [_ X / m ]_ M )
14 sbceq1a 
 |-  ( x = X -> ( ph <-> [. X / x ]. ph ) )
15 13 14 rabeqbidv 
 |-  ( x = X -> { y e. [_ x / m ]_ M | ph } = { y e. [_ X / m ]_ M | [. X / x ]. ph } )
16 8 12 15 1 fvmptf 
 |-  ( ( X e. V /\ { y e. [_ X / m ]_ M | [. X / x ]. ph } e. _V ) -> ( F ` X ) = { y e. [_ X / m ]_ M | [. X / x ]. ph } )
17 5 7 16 syl2anc 
 |-  ( X e. dom F -> ( F ` X ) = { y e. [_ X / m ]_ M | [. X / x ]. ph } )
18 17 eleq2d 
 |-  ( X e. dom F -> ( Y e. ( F ` X ) <-> Y e. { y e. [_ X / m ]_ M | [. X / x ]. ph } ) )
19 elrabi 
 |-  ( Y e. { y e. [_ X / m ]_ M | [. X / x ]. ph } -> Y e. [_ X / m ]_ M )
20 5 19 anim12i 
 |-  ( ( X e. dom F /\ Y e. { y e. [_ X / m ]_ M | [. X / x ]. ph } ) -> ( X e. V /\ Y e. [_ X / m ]_ M ) )
21 20 ex 
 |-  ( X e. dom F -> ( Y e. { y e. [_ X / m ]_ M | [. X / x ]. ph } -> ( X e. V /\ Y e. [_ X / m ]_ M ) ) )
22 18 21 sylbid 
 |-  ( X e. dom F -> ( Y e. ( F ` X ) -> ( X e. V /\ Y e. [_ X / m ]_ M ) ) )
23 3 22 mpcom 
 |-  ( Y e. ( F ` X ) -> ( X e. V /\ Y e. [_ X / m ]_ M ) )