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	11 12	syl	⊢ ( 𝑓 Fn ℕ0 → dom 𝑓 ⊆ ℕ0 )
14	9 10 13	3syl	⊢ ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑓 ∈ 𝑀 ) → dom 𝑓 ⊆ ℕ0 )
15	14	3ad2antl1	⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑓 ∈ 𝑀 ) → dom 𝑓 ⊆ ℕ0 )
16	8 15	sstrid	⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑓 ∈ 𝑀 ) → ( 𝑓 supp 𝑍 ) ⊆ ℕ0 )
17	16	sseld	⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑓 ∈ 𝑀 ) → ( 𝑥 ∈ ( 𝑓 supp 𝑍 ) → 𝑥 ∈ ℕ0 ) )
18	17	adantlr	⊢ ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) → ( 𝑥 ∈ ( 𝑓 supp 𝑍 ) → 𝑥 ∈ ℕ0 ) )
19	18	imp	⊢ ( ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → 𝑥 ∈ ℕ0 )
20	1 2	fsuppmapnn0fiublem	⊢ ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) → ( ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) → 𝑆 ∈ ℕ0 ) )
21	20	imp	⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) → 𝑆 ∈ ℕ0 )
22	21	ad2antrr	⊢ ( ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → 𝑆 ∈ ℕ0 )
23	9 10 11	3syl	⊢ ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑓 ∈ 𝑀 ) → dom 𝑓 = ℕ0 )
24	23	ex	⊢ ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) → ( 𝑓 ∈ 𝑀 → dom 𝑓 = ℕ0 ) )
25	24	3ad2ant1	⊢ ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) → ( 𝑓 ∈ 𝑀 → dom 𝑓 = ℕ0 ) )
26	25	adantr	⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) → ( 𝑓 ∈ 𝑀 → dom 𝑓 = ℕ0 ) )
27	26	imp	⊢ ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) → dom 𝑓 = ℕ0 )
28		nn0ssre	⊢ ℕ0 ⊆ ℝ
29	27 28	eqsstrdi	⊢ ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) → dom 𝑓 ⊆ ℝ )
30	8 29	sstrid	⊢ ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) → ( 𝑓 supp 𝑍 ) ⊆ ℝ )
31	30	ex	⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) → ( 𝑓 ∈ 𝑀 → ( 𝑓 supp 𝑍 ) ⊆ ℝ ) )
32	7 31	ralrimi	⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) → ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ℝ )
33	32	ad2antrr	⊢ ( ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ℝ )
34		iunss	⊢ ( ∪ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ℝ ↔ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ℝ )
35	33 34	sylibr	⊢ ( ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → ∪ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ℝ )
36	1 35	eqsstrid	⊢ ( ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → 𝑈 ⊆ ℝ )
37		simp2	⊢ ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ 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	⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) → ( 𝑀 ∈ Fin ∧ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ∈ Fin ) )
43	42	ad2antrr	⊢ ( ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → ( 𝑀 ∈ Fin ∧ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ∈ Fin ) )
44		iunfi	⊢ ( ( 𝑀 ∈ Fin ∧ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ∈ Fin ) → ∪ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ∈ Fin )
45	43 44	syl	⊢ ( ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → ∪ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ∈ Fin )
46	1 45	eqeltrid	⊢ ( ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ 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	⊢ ( ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → 𝑥 ∈ 𝑈 )
52	2	a1i	⊢ ( ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → 𝑆 = sup ( 𝑈 , ℝ , < ) )
53	36 46 51 52	supfirege	⊢ ( ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → 𝑥 ≤ 𝑆 )
54		elfz2nn0	⊢ ( 𝑥 ∈ ( 0 ... 𝑆 ) ↔ ( 𝑥 ∈ ℕ0 ∧ 𝑆 ∈ ℕ0 ∧ 𝑥 ≤ 𝑆 ) )
55	19 22 53 54	syl3anbrc	⊢ ( ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → 𝑥 ∈ ( 0 ... 𝑆 ) )
56	55	ex	⊢ ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) → ( 𝑥 ∈ ( 𝑓 supp 𝑍 ) → 𝑥 ∈ ( 0 ... 𝑆 ) ) )
57	56	ssrdv	⊢ ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) → ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑆 ) )
58	57	ex	⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) → ( 𝑓 ∈ 𝑀 → ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑆 ) ) )
59	7 58	ralrimi	⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) → ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑆 ) )
60	59	ex	⊢ ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) → ( ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) → ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑆 ) ) )