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

Metamath Proof Explorer

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