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

Metamath Proof Explorer

Theorem abfmpeld

Proof