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 ) )