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

Metamath Proof Explorer

Theorem elfvmptrab1

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. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker elfvmptrab1w when possible. (Contributed by Alexander van der Vekens, 15-Jul-2018) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 elfvmptrab1.f 
 |-  F = ( x e. V |-> { y e. [_ x / m ]_ M | ph } )
2 elfvmptrab1.v 
 |-  ( X e. V -> [_ X / m ]_ M e. _V )
3 ne0i 
 |-  ( Y e. ( F ` X ) -> ( F ` X ) =/= (/) )
4 ndmfv 
 |-  ( -. X e. dom F -> ( F ` X ) = (/) )
5 4 necon1ai 
 |-  ( ( F ` X ) =/= (/) -> X e. dom F )
6 1 dmmptss 
 |-  dom F C_ V
7 6 sseli 
 |-  ( X e. dom F -> X e. V )
8 rabexg 
 |-  ( [_ X / m ]_ M e. _V -> { y e. [_ X / m ]_ M | [. X / x ]. ph } e. _V )
9 7 2 8 3syl 
 |-  ( X e. dom F -> { y e. [_ X / m ]_ M | [. X / x ]. ph } e. _V )
10 nfcv 
 |-  F/_ x X
11 nfsbc1v 
 |-  F/ x [. X / x ]. ph
12 nfcv 
 |-  F/_ x M
13 10 12 nfcsb 
 |-  F/_ x [_ X / m ]_ M
14 11 13 nfrab 
 |-  F/_ x { y e. [_ X / m ]_ M | [. X / x ]. ph }
15 csbeq1 
 |-  ( x = X -> [_ x / m ]_ M = [_ X / m ]_ M )
16 sbceq1a 
 |-  ( x = X -> ( ph <-> [. X / x ]. ph ) )
17 15 16 rabeqbidv 
 |-  ( x = X -> { y e. [_ x / m ]_ M | ph } = { y e. [_ X / m ]_ M | [. X / x ]. ph } )
18 10 14 17 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 } )
19 7 9 18 syl2anc 
 |-  ( X e. dom F -> ( F ` X ) = { y e. [_ X / m ]_ M | [. X / x ]. ph } )
20 19 eleq2d 
 |-  ( X e. dom F -> ( Y e. ( F ` X ) <-> Y e. { y e. [_ X / m ]_ M | [. X / x ]. ph } ) )
21 elrabi 
 |-  ( Y e. { y e. [_ X / m ]_ M | [. X / x ]. ph } -> Y e. [_ X / m ]_ M )
22 7 21 anim12i 
 |-  ( ( X e. dom F /\ Y e. { y e. [_ X / m ]_ M | [. X / x ]. ph } ) -> ( X e. V /\ Y e. [_ X / m ]_ M ) )
23 22 ex 
 |-  ( X e. dom F -> ( Y e. { y e. [_ X / m ]_ M | [. X / x ]. ph } -> ( X e. V /\ Y e. [_ X / m ]_ M ) ) )
24 20 23 sylbid 
 |-  ( X e. dom F -> ( Y e. ( F ` X ) -> ( X e. V /\ Y e. [_ X / m ]_ M ) ) )
25 3 5 24 3syl 
 |-  ( Y e. ( F ` X ) -> ( Y e. ( F ` X ) -> ( X e. V /\ Y e. [_ X / m ]_ M ) ) )
26 25 pm2.43i 
 |-  ( Y e. ( F ` X ) -> ( X e. V /\ Y e. [_ X / m ]_ M ) )