Theorem snelmap

Description: Membership of the element in the range of a constant map. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	snelmap.a	|- ( ph -> A e. V )
	snelmap.b	|- ( ph -> B e. W )
	snelmap.n	|- ( ph -> A =/= (/) )
	snelmap.e	|- ( ph -> ( A X. { x } ) e. ( B ^m A ) )
Assertion	snelmap	|- ( ph -> x e. B )

Proof

Step	Hyp	Ref	Expression
1		snelmap.a	|- ( ph -> A e. V )
2		snelmap.b	|- ( ph -> B e. W )
3		snelmap.n	|- ( ph -> A =/= (/) )
4		snelmap.e	|- ( ph -> ( A X. { x } ) e. ( B ^m A ) )
5		n0	|- ( A =/= (/) <-> E. y y e. A )
6	3 5	sylib	|- ( ph -> E. y y e. A )
7		vex	|- x e. _V
8	7	fvconst2	|- ( y e. A -> ( ( A X. { x } ) ` y ) = x )
9	8	eqcomd	|- ( y e. A -> x = ( ( A X. { x } ) ` y ) )
10	9	adantl	|- ( ( ph /\ y e. A ) -> x = ( ( A X. { x } ) ` y ) )
11		elmapg	|- ( ( B e. W /\ A e. V ) -> ( ( A X. { x } ) e. ( B ^m A ) <-> ( A X. { x } ) : A --> B ) )
12	2 1 11	syl2anc	|- ( ph -> ( ( A X. { x } ) e. ( B ^m A ) <-> ( A X. { x } ) : A --> B ) )
13	4 12	mpbid	|- ( ph -> ( A X. { x } ) : A --> B )
14	13	adantr	|- ( ( ph /\ y e. A ) -> ( A X. { x } ) : A --> B )
15		simpr	|- ( ( ph /\ y e. A ) -> y e. A )
16	14 15	ffvelrnd	|- ( ( ph /\ y e. A ) -> ( ( A X. { x } ) ` y ) e. B )
17	10 16	eqeltrd	|- ( ( ph /\ y e. A ) -> x e. B )
18	17	ex	|- ( ph -> ( y e. A -> x e. B ) )
19	18	exlimdv	|- ( ph -> ( E. y y e. A -> x e. B ) )
20	6 19	mpd	|- ( ph -> x e. B )