Metamath Proof Explorer


Theorem fsuppmapnn0fiub

Description: If all functions of a finite set of functions over the nonnegative integers are finitely supported, then the support of all these functions is contained in a finite set of sequential integers starting at 0 and ending with the supremum of the union of the support of these functions. (Contributed by AV, 2-Oct-2019) (Proof shortened by JJ, 2-Aug-2021)

Ref Expression
Hypotheses fsuppmapnn0fiub.u 𝑈 = 𝑓𝑀 ( 𝑓 supp 𝑍 )
fsuppmapnn0fiub.s 𝑆 = sup ( 𝑈 , ℝ , < )
Assertion fsuppmapnn0fiub ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) → ( ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍𝑈 ≠ ∅ ) → ∀ 𝑓𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 fsuppmapnn0fiub.u 𝑈 = 𝑓𝑀 ( 𝑓 supp 𝑍 )
2 fsuppmapnn0fiub.s 𝑆 = sup ( 𝑈 , ℝ , < )
3 nfv 𝑓 ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 )
4 nfra1 𝑓𝑓𝑀 𝑓 finSupp 𝑍
5 nfv 𝑓 𝑈 ≠ ∅
6 4 5 nfan 𝑓 ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍𝑈 ≠ ∅ )
7 3 6 nfan 𝑓 ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍𝑈 ≠ ∅ ) )
8 suppssdm ( 𝑓 supp 𝑍 ) ⊆ dom 𝑓
9 ssel2 ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑓𝑀 ) → 𝑓 ∈ ( 𝑅m0 ) )
10 elmapfn ( 𝑓 ∈ ( 𝑅m0 ) → 𝑓 Fn ℕ0 )
11 fndm ( 𝑓 Fn ℕ0 → dom 𝑓 = ℕ0 )
12 eqimss ( dom 𝑓 = ℕ0 → dom 𝑓 ⊆ ℕ0 )
13 11 12 syl ( 𝑓 Fn ℕ0 → dom 𝑓 ⊆ ℕ0 )
14 9 10 13 3syl ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑓𝑀 ) → dom 𝑓 ⊆ ℕ0 )
15 14 3ad2antl1 ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ 𝑓𝑀 ) → dom 𝑓 ⊆ ℕ0 )
16 8 15 sstrid ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ 𝑓𝑀 ) → ( 𝑓 supp 𝑍 ) ⊆ ℕ0 )
17 16 sseld ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ 𝑓𝑀 ) → ( 𝑥 ∈ ( 𝑓 supp 𝑍 ) → 𝑥 ∈ ℕ0 ) )
18 17 adantlr ( ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍𝑈 ≠ ∅ ) ) ∧ 𝑓𝑀 ) → ( 𝑥 ∈ ( 𝑓 supp 𝑍 ) → 𝑥 ∈ ℕ0 ) )
19 18 imp ( ( ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍𝑈 ≠ ∅ ) ) ∧ 𝑓𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → 𝑥 ∈ ℕ0 )
20 1 2 fsuppmapnn0fiublem ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) → ( ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍𝑈 ≠ ∅ ) → 𝑆 ∈ ℕ0 ) )
21 20 imp ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍𝑈 ≠ ∅ ) ) → 𝑆 ∈ ℕ0 )
22 21 ad2antrr ( ( ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍𝑈 ≠ ∅ ) ) ∧ 𝑓𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → 𝑆 ∈ ℕ0 )
23 9 10 11 3syl ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑓𝑀 ) → dom 𝑓 = ℕ0 )
24 23 ex ( 𝑀 ⊆ ( 𝑅m0 ) → ( 𝑓𝑀 → dom 𝑓 = ℕ0 ) )
25 24 3ad2ant1 ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) → ( 𝑓𝑀 → dom 𝑓 = ℕ0 ) )
26 25 adantr ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍𝑈 ≠ ∅ ) ) → ( 𝑓𝑀 → dom 𝑓 = ℕ0 ) )
27 26 imp ( ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍𝑈 ≠ ∅ ) ) ∧ 𝑓𝑀 ) → dom 𝑓 = ℕ0 )
28 nn0ssre 0 ⊆ ℝ
29 27 28 eqsstrdi ( ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍𝑈 ≠ ∅ ) ) ∧ 𝑓𝑀 ) → dom 𝑓 ⊆ ℝ )
30 8 29 sstrid ( ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍𝑈 ≠ ∅ ) ) ∧ 𝑓𝑀 ) → ( 𝑓 supp 𝑍 ) ⊆ ℝ )
31 30 ex ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍𝑈 ≠ ∅ ) ) → ( 𝑓𝑀 → ( 𝑓 supp 𝑍 ) ⊆ ℝ ) )
32 7 31 ralrimi ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍𝑈 ≠ ∅ ) ) → ∀ 𝑓𝑀 ( 𝑓 supp 𝑍 ) ⊆ ℝ )
33 32 ad2antrr ( ( ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍𝑈 ≠ ∅ ) ) ∧ 𝑓𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → ∀ 𝑓𝑀 ( 𝑓 supp 𝑍 ) ⊆ ℝ )
34 iunss ( 𝑓𝑀 ( 𝑓 supp 𝑍 ) ⊆ ℝ ↔ ∀ 𝑓𝑀 ( 𝑓 supp 𝑍 ) ⊆ ℝ )
35 33 34 sylibr ( ( ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍𝑈 ≠ ∅ ) ) ∧ 𝑓𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → 𝑓𝑀 ( 𝑓 supp 𝑍 ) ⊆ ℝ )
36 1 35 eqsstrid ( ( ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍𝑈 ≠ ∅ ) ) ∧ 𝑓𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → 𝑈 ⊆ ℝ )
37 simp2 ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) → 𝑀 ∈ Fin )
38 id ( 𝑓 finSupp 𝑍𝑓 finSupp 𝑍 )
39 38 fsuppimpd ( 𝑓 finSupp 𝑍 → ( 𝑓 supp 𝑍 ) ∈ Fin )
40 39 ralimi ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍 → ∀ 𝑓𝑀 ( 𝑓 supp 𝑍 ) ∈ Fin )
41 40 adantr ( ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍𝑈 ≠ ∅ ) → ∀ 𝑓𝑀 ( 𝑓 supp 𝑍 ) ∈ Fin )
42 37 41 anim12i ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍𝑈 ≠ ∅ ) ) → ( 𝑀 ∈ Fin ∧ ∀ 𝑓𝑀 ( 𝑓 supp 𝑍 ) ∈ Fin ) )
43 42 ad2antrr ( ( ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍𝑈 ≠ ∅ ) ) ∧ 𝑓𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → ( 𝑀 ∈ Fin ∧ ∀ 𝑓𝑀 ( 𝑓 supp 𝑍 ) ∈ Fin ) )
44 iunfi ( ( 𝑀 ∈ Fin ∧ ∀ 𝑓𝑀 ( 𝑓 supp 𝑍 ) ∈ Fin ) → 𝑓𝑀 ( 𝑓 supp 𝑍 ) ∈ Fin )
45 43 44 syl ( ( ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍𝑈 ≠ ∅ ) ) ∧ 𝑓𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → 𝑓𝑀 ( 𝑓 supp 𝑍 ) ∈ Fin )
46 1 45 eqeltrid ( ( ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍𝑈 ≠ ∅ ) ) ∧ 𝑓𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → 𝑈 ∈ Fin )
47 rspe ( ( 𝑓𝑀𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → ∃ 𝑓𝑀 𝑥 ∈ ( 𝑓 supp 𝑍 ) )
48 eliun ( 𝑥 𝑓𝑀 ( 𝑓 supp 𝑍 ) ↔ ∃ 𝑓𝑀 𝑥 ∈ ( 𝑓 supp 𝑍 ) )
49 47 48 sylibr ( ( 𝑓𝑀𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → 𝑥 𝑓𝑀 ( 𝑓 supp 𝑍 ) )
50 49 1 eleqtrrdi ( ( 𝑓𝑀𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → 𝑥𝑈 )
51 50 adantll ( ( ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍𝑈 ≠ ∅ ) ) ∧ 𝑓𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → 𝑥𝑈 )
52 2 a1i ( ( ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍𝑈 ≠ ∅ ) ) ∧ 𝑓𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → 𝑆 = sup ( 𝑈 , ℝ , < ) )
53 36 46 51 52 supfirege ( ( ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍𝑈 ≠ ∅ ) ) ∧ 𝑓𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → 𝑥𝑆 )
54 elfz2nn0 ( 𝑥 ∈ ( 0 ... 𝑆 ) ↔ ( 𝑥 ∈ ℕ0𝑆 ∈ ℕ0𝑥𝑆 ) )
55 19 22 53 54 syl3anbrc ( ( ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍𝑈 ≠ ∅ ) ) ∧ 𝑓𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → 𝑥 ∈ ( 0 ... 𝑆 ) )
56 55 ex ( ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍𝑈 ≠ ∅ ) ) ∧ 𝑓𝑀 ) → ( 𝑥 ∈ ( 𝑓 supp 𝑍 ) → 𝑥 ∈ ( 0 ... 𝑆 ) ) )
57 56 ssrdv ( ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍𝑈 ≠ ∅ ) ) ∧ 𝑓𝑀 ) → ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑆 ) )
58 57 ex ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍𝑈 ≠ ∅ ) ) → ( 𝑓𝑀 → ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑆 ) ) )
59 7 58 ralrimi ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍𝑈 ≠ ∅ ) ) → ∀ 𝑓𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑆 ) )
60 59 ex ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) → ( ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍𝑈 ≠ ∅ ) → ∀ 𝑓𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑆 ) ) )