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 V Y W Z U finSupp Z X Y

Proof

Step Hyp Ref Expression
1 snfi X Fin
2 snopsuppss X Y supp Z X
3 1 2 pm3.2i X Fin X Y supp Z X
4 ssfi X Fin X Y supp Z X X Y supp Z Fin
5 3 4 mp1i X V Y W Z U X Y supp Z Fin
6 funsng X V Y W Fun X Y
7 6 3adant3 X V Y W Z U Fun X Y
8 snex X Y V
9 8 a1i X V Y W Z U X Y V
10 simp3 X V Y W Z U Z U
11 funisfsupp Fun X Y X Y V Z U finSupp Z X Y X Y supp Z Fin
12 7 9 10 11 syl3anc X V Y W Z U finSupp Z X Y X Y supp Z Fin
13 5 12 mpbird X V Y W Z U finSupp Z X Y