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