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

Metamath Proof Explorer

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 )