Metamath Proof Explorer

Theorem fsuppmapnn0fiubex

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. (Contributed by AV, 2-Oct-2019)

Ref Expression
Assertion fsuppmapnn0fiubex ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) → ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 → ∃ 𝑚 ∈ ℕ0 ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) ) )

Proof

Step Hyp Ref Expression
1 0nn0 ⊢ 0 ∈ ℕ0
2 1 a1i ⊢ ( ( ∅ = 𝑀 ∨ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) → 0 ∈ ℕ0 )
3 oveq2 ⊢ ( 𝑚 = 0 → ( 0 ... 𝑚 ) = ( 0 ... 0 ) )
4 3 sseq2d ⊢ ( 𝑚 = 0 → ( ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) ↔ ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 0 ) ) )
5 4 ralbidv ⊢ ( 𝑚 = 0 → ( ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) ↔ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 0 ) ) )
6 5 adantl ⊢ ( ( ( ∅ = 𝑀 ∨ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ∧ 𝑚 = 0 ) → ( ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) ↔ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 0 ) ) )
7 ral0 ⊢ ∀ 𝑓 ∈ ∅ ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 0 )
8 raleq ⊢ ( ∅ = 𝑀 → ( ∀ 𝑓 ∈ ∅ ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 0 ) ↔ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 0 ) ) )
9 7 8 mpbii ⊢ ( ∅ = 𝑀 → ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 0 ) )
10 0ss ⊢ ∅ ⊆ ( 0 ... 0 )
11 sseq1 ⊢ ( ( 𝑓 supp 𝑍 ) = ∅ → ( ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 0 ) ↔ ∅ ⊆ ( 0 ... 0 ) ) )
12 10 11 mpbiri ⊢ ( ( 𝑓 supp 𝑍 ) = ∅ → ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 0 ) )
13 12 ralimi ⊢ ( ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ → ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 0 ) )
14 9 13 jaoi ⊢ ( ( ∅ = 𝑀 ∨ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) → ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 0 ) )
15 2 6 14 rspcedvd ⊢ ( ( ∅ = 𝑀 ∨ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) → ∃ 𝑚 ∈ ℕ0 ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) )
16 15 2a1d ⊢ ( ( ∅ = 𝑀 ∨ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) → ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) → ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 → ∃ 𝑚 ∈ ℕ0 ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) ) ) )
17 simplr ⊢ ( ( ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ) ∧ ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ) → ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) )
18 simpr ⊢ ( ( ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ) ∧ ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ) → ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 )
19 ioran ⊢ ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ↔ ( ¬ ∅ = 𝑀 ∧ ¬ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) )
20 oveq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 supp 𝑍 ) = ( 𝑔 supp 𝑍 ) )
21 20 eqeq1d ⊢ ( 𝑓 = 𝑔 → ( ( 𝑓 supp 𝑍 ) = ∅ ↔ ( 𝑔 supp 𝑍 ) = ∅ ) )
22 21 cbvralvw ⊢ ( ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ ↔ ∀ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) = ∅ )
23 22 notbii ⊢ ( ¬ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ ↔ ¬ ∀ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) = ∅ )
24 23 anbi2i ⊢ ( ( ¬ ∅ = 𝑀 ∧ ¬ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ↔ ( ¬ ∅ = 𝑀 ∧ ¬ ∀ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) = ∅ ) )
25 19 24 bitri ⊢ ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ↔ ( ¬ ∅ = 𝑀 ∧ ¬ ∀ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) = ∅ ) )
26 rexnal ⊢ ( ∃ 𝑔 ∈ 𝑀 ¬ ( 𝑔 supp 𝑍 ) = ∅ ↔ ¬ ∀ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) = ∅ )
27 df-ne ⊢ ( ( 𝑔 supp 𝑍 ) ≠ ∅ ↔ ¬ ( 𝑔 supp 𝑍 ) = ∅ )
28 27 bicomi ⊢ ( ¬ ( 𝑔 supp 𝑍 ) = ∅ ↔ ( 𝑔 supp 𝑍 ) ≠ ∅ )
29 28 rexbii ⊢ ( ∃ 𝑔 ∈ 𝑀 ¬ ( 𝑔 supp 𝑍 ) = ∅ ↔ ∃ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) ≠ ∅ )
30 26 29 sylbb1 ⊢ ( ¬ ∀ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) = ∅ → ∃ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) ≠ ∅ )
31 25 30 simplbiim ⊢ ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) → ∃ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) ≠ ∅ )
32 31 ad2antrr ⊢ ( ( ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ) ∧ ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ) → ∃ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) ≠ ∅ )
33 iunn0 ⊢ ( ∃ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) ≠ ∅ ↔ ∪ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) ≠ ∅ )
34 32 33 sylib ⊢ ( ( ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ) ∧ ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ) → ∪ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) ≠ ∅ )
35 18 34 jca ⊢ ( ( ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ) ∧ ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ) → ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ ∪ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) ≠ ∅ ) )
36 oveq1 ⊢ ( 𝑔 = 𝑓 → ( 𝑔 supp 𝑍 ) = ( 𝑓 supp 𝑍 ) )
37 36 cbviunv ⊢ ∪ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) = ∪ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 )
38 eqid ⊢ sup ( ∪ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) , ℝ , < ) = sup ( ∪ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) , ℝ , < )
39 37 38 fsuppmapnn0fiublem ⊢ ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) → ( ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ ∪ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) ≠ ∅ ) → sup ( ∪ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) , ℝ , < ) ∈ ℕ0 ) )
40 17 35 39 sylc ⊢ ( ( ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ) ∧ ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ) → sup ( ∪ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) , ℝ , < ) ∈ ℕ0 )
41 nfv ⊢ Ⅎ 𝑓 ∅ = 𝑀
42 nfra1 ⊢ Ⅎ 𝑓 ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅
43 41 42 nfor ⊢ Ⅎ 𝑓 ( ∅ = 𝑀 ∨ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ )
44 43 nfn ⊢ Ⅎ 𝑓 ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ )
45 nfv ⊢ Ⅎ 𝑓 ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 )
46 44 45 nfan ⊢ Ⅎ 𝑓 ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) )
47 nfra1 ⊢ Ⅎ 𝑓 ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍
48 46 47 nfan ⊢ Ⅎ 𝑓 ( ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ) ∧ ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 )
49 nfv ⊢ Ⅎ 𝑓 𝑚 = sup ( ∪ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) , ℝ , < )
50 48 49 nfan ⊢ Ⅎ 𝑓 ( ( ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ) ∧ ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ) ∧ 𝑚 = sup ( ∪ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) , ℝ , < ) )
51 oveq2 ⊢ ( 𝑚 = sup ( ∪ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) , ℝ , < ) → ( 0 ... 𝑚 ) = ( 0 ... sup ( ∪ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) , ℝ , < ) ) )
52 51 sseq2d ⊢ ( 𝑚 = sup ( ∪ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) , ℝ , < ) → ( ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) ↔ ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... sup ( ∪ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) , ℝ , < ) ) ) )
53 52 adantl ⊢ ( ( ( ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ) ∧ ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ) ∧ 𝑚 = sup ( ∪ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) , ℝ , < ) ) → ( ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) ↔ ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... sup ( ∪ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) , ℝ , < ) ) ) )
54 50 53 ralbid ⊢ ( ( ( ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ) ∧ ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ) ∧ 𝑚 = sup ( ∪ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) , ℝ , < ) ) → ( ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) ↔ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... sup ( ∪ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) , ℝ , < ) ) ) )
55 rexnal ⊢ ( ∃ 𝑓 ∈ 𝑀 ¬ ( 𝑓 supp 𝑍 ) = ∅ ↔ ¬ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ )
56 df-ne ⊢ ( ( 𝑓 supp 𝑍 ) ≠ ∅ ↔ ¬ ( 𝑓 supp 𝑍 ) = ∅ )
57 56 bicomi ⊢ ( ¬ ( 𝑓 supp 𝑍 ) = ∅ ↔ ( 𝑓 supp 𝑍 ) ≠ ∅ )
58 57 rexbii ⊢ ( ∃ 𝑓 ∈ 𝑀 ¬ ( 𝑓 supp 𝑍 ) = ∅ ↔ ∃ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ≠ ∅ )
59 55 58 sylbb1 ⊢ ( ¬ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ → ∃ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ≠ ∅ )
60 19 59 simplbiim ⊢ ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) → ∃ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ≠ ∅ )
61 60 ad2antrr ⊢ ( ( ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ) ∧ ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ) → ∃ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ≠ ∅ )
62 iunn0 ⊢ ( ∃ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ≠ ∅ ↔ ∪ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ≠ ∅ )
63 20 cbviunv ⊢ ∪ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∪ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 )
64 63 neeq1i ⊢ ( ∪ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ≠ ∅ ↔ ∪ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) ≠ ∅ )
65 62 64 bitri ⊢ ( ∃ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ≠ ∅ ↔ ∪ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) ≠ ∅ )
66 61 65 sylib ⊢ ( ( ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ) ∧ ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ) → ∪ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) ≠ ∅ )
67 18 66 jca ⊢ ( ( ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ) ∧ ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ) → ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ ∪ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) ≠ ∅ ) )
68 37 38 fsuppmapnn0fiub ⊢ ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) → ( ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ ∪ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) ≠ ∅ ) → ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... sup ( ∪ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) , ℝ , < ) ) ) )
69 17 67 68 sylc ⊢ ( ( ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ) ∧ ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ) → ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... sup ( ∪ 𝑔 ∈ 𝑀 ( 𝑔 supp 𝑍 ) , ℝ , < ) ) )
70 40 54 69 rspcedvd ⊢ ( ( ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ) ∧ ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ) → ∃ 𝑚 ∈ ℕ0 ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) )
71 70 exp31 ⊢ ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) → ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) → ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 → ∃ 𝑚 ∈ ℕ0 ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) ) ) )
72 16 71 pm2.61i ⊢ ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) → ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 → ∃ 𝑚 ∈ ℕ0 ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) ) )