Theorem abfmpeld

Description: Membership in an element of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 19-Oct-2016)

	Ref	Expression
Hypotheses	abfmpeld.1	|- F = ( x e. V |-> { y | ps } )
	abfmpeld.2	|- ( ph -> { y | ps } e. _V )
	abfmpeld.3	|- ( ph -> ( ( x = A /\ y = B ) -> ( ps <-> ch ) ) )
Assertion	abfmpeld	|- ( ph -> ( ( A e. V /\ B e. W ) -> ( B e. ( F ` A ) <-> ch ) ) )

Proof

Step	Hyp	Ref	Expression
1		abfmpeld.1	|- F = ( x e. V |-> { y | ps } )
2		abfmpeld.2	|- ( ph -> { y | ps } e. _V )
3		abfmpeld.3	|- ( ph -> ( ( x = A /\ y = B ) -> ( ps <-> ch ) ) )
4	2	alrimiv	|- ( ph -> A. x { y | ps } e. _V )
5		csbexg	|- ( A. x { y | ps } e. _V -> [_ A / x ]_ { y | ps } e. _V )
6	4 5	syl	|- ( ph -> [_ A / x ]_ { y | ps } e. _V )
7	1	fvmpts	|- ( ( A e. V /\ [_ A / x ]_ { y | ps } e. _V ) -> ( F ` A ) = [_ A / x ]_ { y | ps } )
8	6 7	sylan2	|- ( ( A e. V /\ ph ) -> ( F ` A ) = [_ A / x ]_ { y | ps } )
9		csbab	|- [_ A / x ]_ { y | ps } = { y | [. A / x ]. ps }
10	8 9	eqtrdi	|- ( ( A e. V /\ ph ) -> ( F ` A ) = { y | [. A / x ]. ps } )
11	10	eleq2d	|- ( ( A e. V /\ ph ) -> ( B e. ( F ` A ) <-> B e. { y | [. A / x ]. ps } ) )
12	11	adantl	|- ( ( B e. W /\ ( A e. V /\ ph ) ) -> ( B e. ( F ` A ) <-> B e. { y | [. A / x ]. ps } ) )
13		simpll	|- ( ( ( A e. V /\ ph ) /\ y = B ) -> A e. V )
14	3	ancomsd	|- ( ph -> ( ( y = B /\ x = A ) -> ( ps <-> ch ) ) )
15	14	adantl	|- ( ( A e. V /\ ph ) -> ( ( y = B /\ x = A ) -> ( ps <-> ch ) ) )
16	15	impl	|- ( ( ( ( A e. V /\ ph ) /\ y = B ) /\ x = A ) -> ( ps <-> ch ) )
17	13 16	sbcied	|- ( ( ( A e. V /\ ph ) /\ y = B ) -> ( [. A / x ]. ps <-> ch ) )
18	17	ex	|- ( ( A e. V /\ ph ) -> ( y = B -> ( [. A / x ]. ps <-> ch ) ) )
19	18	alrimiv	|- ( ( A e. V /\ ph ) -> A. y ( y = B -> ( [. A / x ]. ps <-> ch ) ) )
20		elabgt	|- ( ( B e. W /\ A. y ( y = B -> ( [. A / x ]. ps <-> ch ) ) ) -> ( B e. { y | [. A / x ]. ps } <-> ch ) )
21	19 20	sylan2	|- ( ( B e. W /\ ( A e. V /\ ph ) ) -> ( B e. { y | [. A / x ]. ps } <-> ch ) )
22	12 21	bitrd	|- ( ( B e. W /\ ( A e. V /\ ph ) ) -> ( B e. ( F ` A ) <-> ch ) )
23	22	an13s	|- ( ( ph /\ ( A e. V /\ B e. W ) ) -> ( B e. ( F ` A ) <-> ch ) )
24	23	ex	|- ( ph -> ( ( A e. V /\ B e. W ) -> ( B e. ( F ` A ) <-> ch ) ) )