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

Metamath Proof Explorer

Theorem mptnn0fsuppd

Description: A mapping from the nonnegative integers is finitely supported under certain conditions. (Contributed by AV, 2-Dec-2019) (Revised by AV, 23-Dec-2019)

		Ref	Expression
	Hypotheses	mptnn0fsupp.0	$⊢ φ \to \underset{˙}{0} \in V$
		mptnn0fsupp.c	$⊢ (φ \land k \in ℕ_{0}) \to C \in B$
		mptnn0fsuppd.d	$⊢ k = x \to C = D$
		mptnn0fsuppd.s	$⊢ φ \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to D = \underset{˙}{0})$
	Assertion	mptnn0fsuppd	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((k \in ℕ_{0} ⟼ C))$

Proof

Step	Hyp	Ref	Expression
1		mptnn0fsupp.0	$⊢ φ \to \underset{˙}{0} \in V$
2		mptnn0fsupp.c	$⊢ (φ \land k \in ℕ_{0}) \to C \in B$
3		mptnn0fsuppd.d	$⊢ k = x \to C = D$
4		mptnn0fsuppd.s	$⊢ φ \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to D = \underset{˙}{0})$
5		vex	$⊢ x \in V$
6	5 3	csbie	$⊢ ⦋ x / k ⦌ C = D$
7		id	$⊢ D = \underset{˙}{0} \to D = \underset{˙}{0}$
8	6 7	eqtrid	$⊢ D = \underset{˙}{0} \to ⦋ x / k ⦌ C = \underset{˙}{0}$
9	8	imim2i	$⊢ (s < x \to D = \underset{˙}{0}) \to (s < x \to ⦋ x / k ⦌ C = \underset{˙}{0})$
10	9	ralimi	$⊢ \forall x \in ℕ_{0} (s < x \to D = \underset{˙}{0}) \to \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ C = \underset{˙}{0})$
11	10	reximi	$⊢ \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to D = \underset{˙}{0}) \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ C = \underset{˙}{0})$
12	4 11	syl	$⊢ φ \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ C = \underset{˙}{0})$
13	1 2 12	mptnn0fsupp	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((k \in ℕ_{0} ⟼ C))$