snopfsupp

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

		Ref	Expression
	Assertion	snopfsupp	$⊢ (X \in V \land Y \in W \land Z \in U) \to {finSupp}_{Z} (\{⟨X, Y⟩\})$

Step	Hyp	Ref	Expression
1		snfi	$⊢ \{X\} \in Fin$
2		snopsuppss	$⊢ \{⟨X, Y⟩\} supp Z \subseteq \{X\}$
3	1 2	pm3.2i	$⊢ (\{X\} \in Fin \land \{⟨X, Y⟩\} supp Z \subseteq \{X\})$
4		ssfi	$⊢ (\{X\} \in Fin \land \{⟨X, Y⟩\} supp Z \subseteq \{X\}) \to \{⟨X, Y⟩\} supp Z \in Fin$
5	3 4	mp1i	$⊢ (X \in V \land Y \in W \land Z \in U) \to \{⟨X, Y⟩\} supp Z \in Fin$
6		funsng	$⊢ (X \in V \land Y \in W) \to Fun \{⟨X, Y⟩\}$
7	6	3adant3	$⊢ (X \in V \land Y \in W \land Z \in U) \to Fun \{⟨X, Y⟩\}$
8		snex	$⊢ \{⟨X, Y⟩\} \in V$
9	8	a1i	$⊢ (X \in V \land Y \in W \land Z \in U) \to \{⟨X, Y⟩\} \in V$
10		simp3	$⊢ (X \in V \land Y \in W \land Z \in U) \to Z \in U$
11		funisfsupp	$⊢ (Fun \{⟨X, Y⟩\} \land \{⟨X, Y⟩\} \in V \land Z \in U) \to ({finSupp}_{Z} (\{⟨X, Y⟩\}) \leftrightarrow \{⟨X, Y⟩\} supp Z \in Fin)$
12	7 9 10 11	syl3anc	$⊢ (X \in V \land Y \in W \land Z \in U) \to ({finSupp}_{Z} (\{⟨X, Y⟩\}) \leftrightarrow \{⟨X, Y⟩\} supp Z \in Fin)$
13	5 12	mpbird	$⊢ (X \in V \land Y \in W \land Z \in U) \to {finSupp}_{Z} (\{⟨X, Y⟩\})$

Metamath Proof Explorer