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

Metamath Proof Explorer

Theorem mptnn0fsupp

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

Ref Expression
Hypotheses mptnn0fsupp.0 ⊢ ( 𝜑 → 0 ∈ 𝑉 )
mptnn0fsupp.c ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐶 ∈ 𝐵 )
mptnn0fsupp.s ⊢ ( 𝜑 → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) )
Assertion mptnn0fsupp ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) finSupp 0 )

Proof

Step Hyp Ref Expression
1 mptnn0fsupp.0 ⊢ ( 𝜑 → 0 ∈ 𝑉 )
2 mptnn0fsupp.c ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐶 ∈ 𝐵 )
3 mptnn0fsupp.s ⊢ ( 𝜑 → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) )
4 2 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 𝐶 ∈ 𝐵 )
5 eqid ⊢ ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) = ( 𝑘 ∈ ℕ0 ↦ 𝐶 )
6 5 fnmpt ⊢ ( ∀ 𝑘 ∈ ℕ0 𝐶 ∈ 𝐵 → ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) Fn ℕ0 )
7 4 6 syl ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) Fn ℕ0 )
8 nn0ex ⊢ ℕ0 ∈ V
9 8 a1i ⊢ ( 𝜑 → ℕ0 ∈ V )
10 1 elexd ⊢ ( 𝜑 → 0 ∈ V )
11 suppvalfn ⊢ ( ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) Fn ℕ0 ∧ ℕ0 ∈ V ∧ 0 ∈ V ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) supp 0 ) = { 𝑥 ∈ ℕ0 ∣ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 0 } )
12 7 9 10 11 syl3anc ⊢ ( 𝜑 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) supp 0 ) = { 𝑥 ∈ ℕ0 ∣ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 0 } )
13 nne ⊢ ( ¬ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 0 ↔ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) = 0 )
14 simpr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → 𝑥 ∈ ℕ0 )
15 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ∀ 𝑘 ∈ ℕ0 𝐶 ∈ 𝐵 )
16 rspcsbela ⊢ ( ( 𝑥 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ℕ0 𝐶 ∈ 𝐵 ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
17 14 15 16 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
18 5 fvmpts ⊢ ( ( 𝑥 ∈ ℕ0 ∧ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ∈ 𝐵 ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) = ⦋ 𝑥 / 𝑘 ⦌ 𝐶 )
19 14 17 18 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) = ⦋ 𝑥 / 𝑘 ⦌ 𝐶 )
20 19 eqeq1d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) = 0 ↔ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) )
21 13 20 bitrid ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ¬ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 0 ↔ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) )
22 21 imbi2d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑠 < 𝑥 → ¬ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 0 ) ↔ ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) ) )
23 22 ralbidva ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ¬ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 0 ) ↔ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) ) )
24 23 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ¬ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 0 ) ↔ ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) ) )
25 3 24 mpbird ⊢ ( 𝜑 → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ¬ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 0 ) )
26 rabssnn0fi ⊢ ( { 𝑥 ∈ ℕ0 ∣ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 0 } ∈ Fin ↔ ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ¬ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 0 ) )
27 25 26 sylibr ⊢ ( 𝜑 → { 𝑥 ∈ ℕ0 ∣ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 0 } ∈ Fin )
28 12 27 eqeltrd ⊢ ( 𝜑 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) supp 0 ) ∈ Fin )
29 funmpt ⊢ Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 )
30 8 mptex ⊢ ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ∈ V
31 funisfsupp ⊢ ( ( Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ∧ ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ∈ V ∧ 0 ∈ V ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) finSupp 0 ↔ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) supp 0 ) ∈ Fin ) )
32 29 30 10 31 mp3an12i ⊢ ( 𝜑 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) finSupp 0 ↔ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) supp 0 ) ∈ Fin ) )
33 28 32 mpbird ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) finSupp 0 )