Theorem mapsnop

Description: A singleton of an ordered pair as an element of the mapping operation. (Contributed by AV, 12-Apr-2019)

	Ref	Expression
Hypothesis	mapsnop.f	|- F = { <. X , Y >. }
Assertion	mapsnop	|- ( ( X e. V /\ Y e. R /\ R e. W ) -> F e. ( R ^m { X } ) )

Proof

Step	Hyp	Ref	Expression
1		mapsnop.f	|- F = { <. X , Y >. }
2		fsng	|- ( ( X e. V /\ Y e. R ) -> ( F : { X } --> { Y } <-> F = { <. X , Y >. } ) )
3	2	3adant3	|- ( ( X e. V /\ Y e. R /\ R e. W ) -> ( F : { X } --> { Y } <-> F = { <. X , Y >. } ) )
4	1 3	mpbiri	|- ( ( X e. V /\ Y e. R /\ R e. W ) -> F : { X } --> { Y } )
5		snssi	|- ( Y e. R -> { Y } C_ R )
6	5	3ad2ant2	|- ( ( X e. V /\ Y e. R /\ R e. W ) -> { Y } C_ R )
7	4 6	fssd	|- ( ( X e. V /\ Y e. R /\ R e. W ) -> F : { X } --> R )
8		simp3	|- ( ( X e. V /\ Y e. R /\ R e. W ) -> R e. W )
9		snex	|- { X } e. _V
10		elmapg	|- ( ( R e. W /\ { X } e. _V ) -> ( F e. ( R ^m { X } ) <-> F : { X } --> R ) )
11	8 9 10	sylancl	|- ( ( X e. V /\ Y e. R /\ R e. W ) -> ( F e. ( R ^m { X } ) <-> F : { X } --> R ) )
12	7 11	mpbird	|- ( ( X e. V /\ Y e. R /\ R e. W ) -> F e. ( R ^m { X } ) )