Theorem snopfsupp

Description: A singleton containing an ordered pair is a finitely supported function. (Contributed by AV, 19-Jul-2019)

	Ref	Expression
Assertion	snopfsupp	|- ( ( X e. V /\ Y e. W /\ Z e. U ) -> { <. X , Y >. } finSupp Z )

Proof

Step	Hyp	Ref	Expression
1		snfi	|- { X } e. Fin
2		snopsuppss	|- ( { <. X , Y >. } supp Z ) C_ { X }
3	1 2	pm3.2i	|- ( { X } e. Fin /\ ( { <. X , Y >. } supp Z ) C_ { X } )
4		ssfi	|- ( ( { X } e. Fin /\ ( { <. X , Y >. } supp Z ) C_ { X } ) -> ( { <. X , Y >. } supp Z ) e. Fin )
5	3 4	mp1i	|- ( ( X e. V /\ Y e. W /\ Z e. U ) -> ( { <. X , Y >. } supp Z ) e. Fin )
6		funsng	|- ( ( X e. V /\ Y e. W ) -> Fun { <. X , Y >. } )
7	6	3adant3	|- ( ( X e. V /\ Y e. W /\ Z e. U ) -> Fun { <. X , Y >. } )
8		snex	|- { <. X , Y >. } e. _V
9	8	a1i	|- ( ( X e. V /\ Y e. W /\ Z e. U ) -> { <. X , Y >. } e. _V )
10		simp3	|- ( ( X e. V /\ Y e. W /\ Z e. U ) -> Z e. U )
11		funisfsupp	|- ( ( Fun { <. X , Y >. } /\ { <. X , Y >. } e. _V /\ Z e. U ) -> ( { <. X , Y >. } finSupp Z <-> ( { <. X , Y >. } supp Z ) e. Fin ) )
12	7 9 10 11	syl3anc	|- ( ( X e. V /\ Y e. W /\ Z e. U ) -> ( { <. X , Y >. } finSupp Z <-> ( { <. X , Y >. } supp Z ) e. Fin ) )
13	5 12	mpbird	|- ( ( X e. V /\ Y e. W /\ Z e. U ) -> { <. X , Y >. } finSupp Z )