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

Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 0 ∈ 𝑉 )
mptnn0fsupp.c ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐶 ∈ 𝐵 )
mptnn0fsuppr.s ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) finSupp 0 )
Assertion mptnn0fsuppr ( 𝜑 → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) )

Proof

Step Hyp Ref Expression
1 mptnn0fsupp.0 ⊢ ( 𝜑 → 0 ∈ 𝑉 )
2 mptnn0fsupp.c ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐶 ∈ 𝐵 )
3 mptnn0fsuppr.s ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) finSupp 0 )
4 fsuppimp ⊢ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) finSupp 0 → ( Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ∧ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) supp 0 ) ∈ Fin ) )
5 2 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 𝐶 ∈ 𝐵 )
6 eqid ⊢ ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) = ( 𝑘 ∈ ℕ0 ↦ 𝐶 )
7 6 fnmpt ⊢ ( ∀ 𝑘 ∈ ℕ0 𝐶 ∈ 𝐵 → ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) Fn ℕ0 )
8 5 7 syl ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) Fn ℕ0 )
9 nn0ex ⊢ ℕ0 ∈ V
10 9 a1i ⊢ ( 𝜑 → ℕ0 ∈ V )
11 1 elexd ⊢ ( 𝜑 → 0 ∈ V )
12 8 10 11 3jca ⊢ ( 𝜑 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) Fn ℕ0 ∧ ℕ0 ∈ V ∧ 0 ∈ V ) )
13 12 adantr ⊢ ( ( 𝜑 ∧ Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) Fn ℕ0 ∧ ℕ0 ∈ V ∧ 0 ∈ V ) )
14 suppvalfn ⊢ ( ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) Fn ℕ0 ∧ ℕ0 ∈ V ∧ 0 ∈ V ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) supp 0 ) = { 𝑥 ∈ ℕ0 ∣ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 0 } )
15 13 14 syl ⊢ ( ( 𝜑 ∧ Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) supp 0 ) = { 𝑥 ∈ ℕ0 ∣ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 0 } )
16 simpr ⊢ ( ( ( 𝜑 ∧ Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ) ∧ 𝑥 ∈ ℕ0 ) → 𝑥 ∈ ℕ0 )
17 5 adantr ⊢ ( ( 𝜑 ∧ Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ) → ∀ 𝑘 ∈ ℕ0 𝐶 ∈ 𝐵 )
18 17 adantr ⊢ ( ( ( 𝜑 ∧ Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ) ∧ 𝑥 ∈ ℕ0 ) → ∀ 𝑘 ∈ ℕ0 𝐶 ∈ 𝐵 )
19 rspcsbela ⊢ ( ( 𝑥 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ℕ0 𝐶 ∈ 𝐵 ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
20 16 18 19 syl2anc ⊢ ( ( ( 𝜑 ∧ Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ) ∧ 𝑥 ∈ ℕ0 ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
21 6 fvmpts ⊢ ( ( 𝑥 ∈ ℕ0 ∧ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ∈ 𝐵 ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) = ⦋ 𝑥 / 𝑘 ⦌ 𝐶 )
22 16 20 21 syl2anc ⊢ ( ( ( 𝜑 ∧ Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) = ⦋ 𝑥 / 𝑘 ⦌ 𝐶 )
23 22 neeq1d ⊢ ( ( ( 𝜑 ∧ Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ) ∧ 𝑥 ∈ ℕ0 ) → ( ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 0 ↔ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 ) )
24 23 rabbidva ⊢ ( ( 𝜑 ∧ Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ) → { 𝑥 ∈ ℕ0 ∣ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 0 } = { 𝑥 ∈ ℕ0 ∣ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 } )
25 15 24 eqtrd ⊢ ( ( 𝜑 ∧ Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) supp 0 ) = { 𝑥 ∈ ℕ0 ∣ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 } )
26 25 eleq1d ⊢ ( ( 𝜑 ∧ Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ) → ( ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) supp 0 ) ∈ Fin ↔ { 𝑥 ∈ ℕ0 ∣ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 } ∈ Fin ) )
27 26 biimpd ⊢ ( ( 𝜑 ∧ Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ) → ( ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) supp 0 ) ∈ Fin → { 𝑥 ∈ ℕ0 ∣ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 } ∈ Fin ) )
28 27 expcom ⊢ ( Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) → ( 𝜑 → ( ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) supp 0 ) ∈ Fin → { 𝑥 ∈ ℕ0 ∣ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 } ∈ Fin ) ) )
29 28 com23 ⊢ ( Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) → ( ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) supp 0 ) ∈ Fin → ( 𝜑 → { 𝑥 ∈ ℕ0 ∣ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 } ∈ Fin ) ) )
30 29 imp ⊢ ( ( Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ∧ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) supp 0 ) ∈ Fin ) → ( 𝜑 → { 𝑥 ∈ ℕ0 ∣ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 } ∈ Fin ) )
31 4 30 syl ⊢ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) finSupp 0 → ( 𝜑 → { 𝑥 ∈ ℕ0 ∣ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 } ∈ Fin ) )
32 3 31 mpcom ⊢ ( 𝜑 → { 𝑥 ∈ ℕ0 ∣ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 } ∈ Fin )
33 rabssnn0fi ⊢ ( { 𝑥 ∈ ℕ0 ∣ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 } ∈ Fin ↔ ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ¬ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 ) )
34 nne ⊢ ( ¬ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 ↔ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 )
35 34 imbi2i ⊢ ( ( 𝑠 < 𝑥 → ¬ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 ) ↔ ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) )
36 35 ralbii ⊢ ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ¬ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 ) ↔ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) )
37 36 rexbii ⊢ ( ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ¬ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 ) ↔ ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) )
38 33 37 bitri ⊢ ( { 𝑥 ∈ ℕ0 ∣ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 } ∈ Fin ↔ ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) )
39 32 38 sylib ⊢ ( 𝜑 → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) )