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	⊢ ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) → ( ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) → ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑆 ) ) )

Proof

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