mptnn0fsuppr

Description: A finitely supported mapping from the nonnegative integers fulfills certain conditions. (Contributed by AV, 3-Nov-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$
	mptnn0fsuppr.s	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((k \in ℕ_{0} ⟼ C))$
Assertion	mptnn0fsuppr	$⊢ φ \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ C = \underset{˙}{0})$

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		mptnn0fsuppr.s	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((k \in ℕ_{0} ⟼ C))$
4		fsuppimp	$⊢ {finSupp}_{\underset{˙}{0}} ((k \in ℕ_{0} ⟼ C)) \to (Fun (k \in ℕ_{0} ⟼ C) \land (k \in ℕ_{0} ⟼ C) supp \underset{˙}{0} \in Fin)$
5	2	ralrimiva	$⊢ φ \to \forall k \in ℕ_{0} C \in B$
6		eqid	$⊢ (k \in ℕ_{0} ⟼ C) = (k \in ℕ_{0} ⟼ C)$
7	6	fnmpt	$⊢ \forall k \in ℕ_{0} C \in B \to (k \in ℕ_{0} ⟼ C) Fn ℕ_{0}$
8	5 7	syl	$⊢ φ \to (k \in ℕ_{0} ⟼ C) Fn ℕ_{0}$
9		nn0ex	$⊢ ℕ_{0} \in V$
10	9	a1i	$⊢ φ \to ℕ_{0} \in V$
11	1	elexd	$⊢ φ \to \underset{˙}{0} \in V$
12	8 10 11	3jca	$⊢ φ \to ((k \in ℕ_{0} ⟼ C) Fn ℕ_{0} \land ℕ_{0} \in V \land \underset{˙}{0} \in V)$
13	12	adantr	$⊢ (φ \land Fun (k \in ℕ_{0} ⟼ C)) \to ((k \in ℕ_{0} ⟼ C) Fn ℕ_{0} \land ℕ_{0} \in V \land \underset{˙}{0} \in V)$
14		suppvalfn	$⊢ ((k \in ℕ_{0} ⟼ C) Fn ℕ_{0} \land ℕ_{0} \in V \land \underset{˙}{0} \in V) \to (k \in ℕ_{0} ⟼ C) supp \underset{˙}{0} = \{x \in ℕ_{0} \| (k \in ℕ_{0} ⟼ C) (x) \neq \underset{˙}{0}\}$
15	13 14	syl	$⊢ (φ \land Fun (k \in ℕ_{0} ⟼ C)) \to (k \in ℕ_{0} ⟼ C) supp \underset{˙}{0} = \{x \in ℕ_{0} \| (k \in ℕ_{0} ⟼ C) (x) \neq \underset{˙}{0}\}$
16		simpr	$⊢ ((φ \land Fun (k \in ℕ_{0} ⟼ C)) \land x \in ℕ_{0}) \to x \in ℕ_{0}$
17	5	adantr	$⊢ (φ \land Fun (k \in ℕ_{0} ⟼ C)) \to \forall k \in ℕ_{0} C \in B$
18	17	adantr	$⊢ ((φ \land Fun (k \in ℕ_{0} ⟼ C)) \land x \in ℕ_{0}) \to \forall k \in ℕ_{0} C \in B$
19		rspcsbela	$⊢ (x \in ℕ_{0} \land \forall k \in ℕ_{0} C \in B) \to ⦋ x / k ⦌ C \in B$
20	16 18 19	syl2anc	$⊢ ((φ \land Fun (k \in ℕ_{0} ⟼ C)) \land x \in ℕ_{0}) \to ⦋ x / k ⦌ C \in B$
21	6	fvmpts	$⊢ (x \in ℕ_{0} \land ⦋ x / k ⦌ C \in B) \to (k \in ℕ_{0} ⟼ C) (x) = ⦋ x / k ⦌ C$
22	16 20 21	syl2anc	$⊢ ((φ \land Fun (k \in ℕ_{0} ⟼ C)) \land x \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ C) (x) = ⦋ x / k ⦌ C$
23	22	neeq1d	$⊢ ((φ \land Fun (k \in ℕ_{0} ⟼ C)) \land x \in ℕ_{0}) \to ((k \in ℕ_{0} ⟼ C) (x) \neq \underset{˙}{0} \leftrightarrow ⦋ x / k ⦌ C \neq \underset{˙}{0})$
24	23	rabbidva	$⊢ (φ \land Fun (k \in ℕ_{0} ⟼ C)) \to \{x \in ℕ_{0} \| (k \in ℕ_{0} ⟼ C) (x) \neq \underset{˙}{0}\} = \{x \in ℕ_{0} \| ⦋ x / k ⦌ C \neq \underset{˙}{0}\}$
25	15 24	eqtrd	$⊢ (φ \land Fun (k \in ℕ_{0} ⟼ C)) \to (k \in ℕ_{0} ⟼ C) supp \underset{˙}{0} = \{x \in ℕ_{0} \| ⦋ x / k ⦌ C \neq \underset{˙}{0}\}$
26	25	eleq1d	$⊢ (φ \land Fun (k \in ℕ_{0} ⟼ C)) \to ((k \in ℕ_{0} ⟼ C) supp \underset{˙}{0} \in Fin \leftrightarrow \{x \in ℕ_{0} \| ⦋ x / k ⦌ C \neq \underset{˙}{0}\} \in Fin)$
27	26	biimpd	$⊢ (φ \land Fun (k \in ℕ_{0} ⟼ C)) \to ((k \in ℕ_{0} ⟼ C) supp \underset{˙}{0} \in Fin \to \{x \in ℕ_{0} \| ⦋ x / k ⦌ C \neq \underset{˙}{0}\} \in Fin)$
28	27	expcom	$⊢ Fun (k \in ℕ_{0} ⟼ C) \to (φ \to ((k \in ℕ_{0} ⟼ C) supp \underset{˙}{0} \in Fin \to \{x \in ℕ_{0} \| ⦋ x / k ⦌ C \neq \underset{˙}{0}\} \in Fin))$
29	28	com23	$⊢ Fun (k \in ℕ_{0} ⟼ C) \to ((k \in ℕ_{0} ⟼ C) supp \underset{˙}{0} \in Fin \to (φ \to \{x \in ℕ_{0} \| ⦋ x / k ⦌ C \neq \underset{˙}{0}\} \in Fin))$
30	29	imp	$⊢ (Fun (k \in ℕ_{0} ⟼ C) \land (k \in ℕ_{0} ⟼ C) supp \underset{˙}{0} \in Fin) \to (φ \to \{x \in ℕ_{0} \| ⦋ x / k ⦌ C \neq \underset{˙}{0}\} \in Fin)$
31	4 30	syl	$⊢ {finSupp}_{\underset{˙}{0}} ((k \in ℕ_{0} ⟼ C)) \to (φ \to \{x \in ℕ_{0} \| ⦋ x / k ⦌ C \neq \underset{˙}{0}\} \in Fin)$
32	3 31	mpcom	$⊢ φ \to \{x \in ℕ_{0} \| ⦋ x / k ⦌ C \neq \underset{˙}{0}\} \in Fin$
33		rabssnn0fi	$⊢ \{x \in ℕ_{0} \| ⦋ x / k ⦌ C \neq \underset{˙}{0}\} \in Fin \leftrightarrow \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to \neg ⦋ x / k ⦌ C \neq \underset{˙}{0})$
34		nne	$⊢ \neg ⦋ x / k ⦌ C \neq \underset{˙}{0} \leftrightarrow ⦋ x / k ⦌ C = \underset{˙}{0}$
35	34	imbi2i	$⊢ (s < x \to \neg ⦋ x / k ⦌ C \neq \underset{˙}{0}) \leftrightarrow (s < x \to ⦋ x / k ⦌ C = \underset{˙}{0})$
36	35	ralbii	$⊢ \forall x \in ℕ_{0} (s < x \to \neg ⦋ x / k ⦌ C \neq \underset{˙}{0}) \leftrightarrow \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ C = \underset{˙}{0})$
37	36	rexbii	$⊢ \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to \neg ⦋ x / k ⦌ C \neq \underset{˙}{0}) \leftrightarrow \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ C = \underset{˙}{0})$
38	33 37	bitri	$⊢ \{x \in ℕ_{0} \| ⦋ x / k ⦌ C \neq \underset{˙}{0}\} \in Fin \leftrightarrow \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ C = \underset{˙}{0})$
39	32 38	sylib	$⊢ φ \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ C = \underset{˙}{0})$

Metamath Proof Explorer

Theorem mptnn0fsuppr

Proof