Theorem fsuppmapnn0fiublem

Description: Lemma for fsuppmapnn0fiub and fsuppmapnn0fiubex . (Contributed by AV, 2-Oct-2019)

	Ref	Expression
Hypotheses	fsuppmapnn0fiub.u	⊢ 𝑈 = ∪ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 )
	fsuppmapnn0fiub.s	⊢ 𝑆 = sup ( 𝑈 , ℝ , < )
Assertion	fsuppmapnn0fiublem	⊢ ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) → ( ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) → 𝑆 ∈ ℕ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	ex	⊢ ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) → ( 𝑓 ∈ 𝑀 → dom 𝑓 ⊆ ℕ0 ) )
16	15	3ad2ant1	⊢ ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) → ( 𝑓 ∈ 𝑀 → dom 𝑓 ⊆ ℕ0 ) )
17	16	adantr	⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) → ( 𝑓 ∈ 𝑀 → dom 𝑓 ⊆ ℕ0 ) )
18	17	imp	⊢ ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) → dom 𝑓 ⊆ ℕ0 )
19	8 18	sstrid	⊢ ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) → ( 𝑓 supp 𝑍 ) ⊆ ℕ0 )
20	19	ex	⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) → ( 𝑓 ∈ 𝑀 → ( 𝑓 supp 𝑍 ) ⊆ ℕ0 ) )
21	7 20	ralrimi	⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) → ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ℕ0 )
22		iunss	⊢ ( ∪ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ℕ0 ↔ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ℕ0 )
23	21 22	sylibr	⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) → ∪ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ℕ0 )
24	1 23	eqsstrid	⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) → 𝑈 ⊆ ℕ0 )
25		ltso	⊢ < Or ℝ
26	25	a1i	⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) → < Or ℝ )
27		simp2	⊢ ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) → 𝑀 ∈ Fin )
28		id	⊢ ( 𝑓 finSupp 𝑍 → 𝑓 finSupp 𝑍 )
29	28	fsuppimpd	⊢ ( 𝑓 finSupp 𝑍 → ( 𝑓 supp 𝑍 ) ∈ Fin )
30	29	ralimi	⊢ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 → ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ∈ Fin )
31	30	adantr	⊢ ( ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) → ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ∈ Fin )
32		iunfi	⊢ ( ( 𝑀 ∈ Fin ∧ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ∈ Fin ) → ∪ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ∈ Fin )
33	27 31 32	syl2an	⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) → ∪ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ∈ Fin )
34	1 33	eqeltrid	⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) → 𝑈 ∈ Fin )
35		simprr	⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) → 𝑈 ≠ ∅ )
36	9 10 11	3syl	⊢ ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑓 ∈ 𝑀 ) → dom 𝑓 = ℕ0 )
37	36	ex	⊢ ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) → ( 𝑓 ∈ 𝑀 → dom 𝑓 = ℕ0 ) )
38	37	3ad2ant1	⊢ ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) → ( 𝑓 ∈ 𝑀 → dom 𝑓 = ℕ0 ) )
39	38	adantr	⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) → ( 𝑓 ∈ 𝑀 → dom 𝑓 = ℕ0 ) )
40	39	imp	⊢ ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) → dom 𝑓 = ℕ0 )
41		nn0ssre	⊢ ℕ0 ⊆ ℝ
42	40 41	eqsstrdi	⊢ ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) → dom 𝑓 ⊆ ℝ )
43	8 42	sstrid	⊢ ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) → ( 𝑓 supp 𝑍 ) ⊆ ℝ )
44	43	ex	⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) → ( 𝑓 ∈ 𝑀 → ( 𝑓 supp 𝑍 ) ⊆ ℝ ) )
45	7 44	ralrimi	⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) → ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ℝ )
46	1	sseq1i	⊢ ( 𝑈 ⊆ ℝ ↔ ∪ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ℝ )
47		iunss	⊢ ( ∪ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ℝ ↔ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ℝ )
48	46 47	bitri	⊢ ( 𝑈 ⊆ ℝ ↔ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ℝ )
49	45 48	sylibr	⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) → 𝑈 ⊆ ℝ )
50		fisupcl	⊢ ( ( < Or ℝ ∧ ( 𝑈 ∈ Fin ∧ 𝑈 ≠ ∅ ∧ 𝑈 ⊆ ℝ ) ) → sup ( 𝑈 , ℝ , < ) ∈ 𝑈 )
51	2 50	eqeltrid	⊢ ( ( < Or ℝ ∧ ( 𝑈 ∈ Fin ∧ 𝑈 ≠ ∅ ∧ 𝑈 ⊆ ℝ ) ) → 𝑆 ∈ 𝑈 )
52	26 34 35 49 51	syl13anc	⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) → 𝑆 ∈ 𝑈 )
53	24 52	sseldd	⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) → 𝑆 ∈ ℕ0 )
54	53	ex	⊢ ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) → ( ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) → 𝑆 ∈ ℕ0 ) )