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 ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ 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 𝑍 ) = ∅ ) → ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) → ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍 → ∃ 𝑚 ∈ ℕ0𝑓𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) ) ) )
17 simplr ( ( ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ) ∧ ∀ 𝑓𝑀 𝑓 finSupp 𝑍 ) → ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) )
18 simpr ( ( ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ 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 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ) ∧ ∀ 𝑓𝑀 𝑓 finSupp 𝑍 ) → ∃ 𝑔𝑀 ( 𝑔 supp 𝑍 ) ≠ ∅ )
33 iunn0 ( ∃ 𝑔𝑀 ( 𝑔 supp 𝑍 ) ≠ ∅ ↔ 𝑔𝑀 ( 𝑔 supp 𝑍 ) ≠ ∅ )
34 32 33 sylib ( ( ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ) ∧ ∀ 𝑓𝑀 𝑓 finSupp 𝑍 ) → 𝑔𝑀 ( 𝑔 supp 𝑍 ) ≠ ∅ )
35 18 34 jca ( ( ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ) ∧ ∀ 𝑓𝑀 𝑓 finSupp 𝑍 ) → ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍 𝑔𝑀 ( 𝑔 supp 𝑍 ) ≠ ∅ ) )
36 oveq1 ( 𝑔 = 𝑓 → ( 𝑔 supp 𝑍 ) = ( 𝑓 supp 𝑍 ) )
37 36 cbviunv 𝑔𝑀 ( 𝑔 supp 𝑍 ) = 𝑓𝑀 ( 𝑓 supp 𝑍 )
38 eqid sup ( 𝑔𝑀 ( 𝑔 supp 𝑍 ) , ℝ , < ) = sup ( 𝑔𝑀 ( 𝑔 supp 𝑍 ) , ℝ , < )
39 37 38 fsuppmapnn0fiublem ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) → ( ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍 𝑔𝑀 ( 𝑔 supp 𝑍 ) ≠ ∅ ) → sup ( 𝑔𝑀 ( 𝑔 supp 𝑍 ) , ℝ , < ) ∈ ℕ0 ) )
40 17 35 39 sylc ( ( ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ) ∧ ∀ 𝑓𝑀 𝑓 finSupp 𝑍 ) → sup ( 𝑔𝑀 ( 𝑔 supp 𝑍 ) , ℝ , < ) ∈ ℕ0 )
41 nfv 𝑓 ∅ = 𝑀
42 nfra1 𝑓𝑓𝑀 ( 𝑓 supp 𝑍 ) = ∅
43 41 42 nfor 𝑓 ( ∅ = 𝑀 ∨ ∀ 𝑓𝑀 ( 𝑓 supp 𝑍 ) = ∅ )
44 43 nfn 𝑓 ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓𝑀 ( 𝑓 supp 𝑍 ) = ∅ )
45 nfv 𝑓 ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 )
46 44 45 nfan 𝑓 ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) )
47 nfra1 𝑓𝑓𝑀 𝑓 finSupp 𝑍
48 46 47 nfan 𝑓 ( ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ) ∧ ∀ 𝑓𝑀 𝑓 finSupp 𝑍 )
49 nfv 𝑓 𝑚 = sup ( 𝑔𝑀 ( 𝑔 supp 𝑍 ) , ℝ , < )
50 48 49 nfan 𝑓 ( ( ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ 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 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ) ∧ ∀ 𝑓𝑀 𝑓 finSupp 𝑍 ) ∧ 𝑚 = sup ( 𝑔𝑀 ( 𝑔 supp 𝑍 ) , ℝ , < ) ) → ( ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) ↔ ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... sup ( 𝑔𝑀 ( 𝑔 supp 𝑍 ) , ℝ , < ) ) ) )
54 50 53 ralbid ( ( ( ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ 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 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ 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 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ) ∧ ∀ 𝑓𝑀 𝑓 finSupp 𝑍 ) → 𝑔𝑀 ( 𝑔 supp 𝑍 ) ≠ ∅ )
67 18 66 jca ( ( ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ) ∧ ∀ 𝑓𝑀 𝑓 finSupp 𝑍 ) → ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍 𝑔𝑀 ( 𝑔 supp 𝑍 ) ≠ ∅ ) )
68 37 38 fsuppmapnn0fiub ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) → ( ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍 𝑔𝑀 ( 𝑔 supp 𝑍 ) ≠ ∅ ) → ∀ 𝑓𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... sup ( 𝑔𝑀 ( 𝑔 supp 𝑍 ) , ℝ , < ) ) ) )
69 17 67 68 sylc ( ( ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ) ∧ ∀ 𝑓𝑀 𝑓 finSupp 𝑍 ) → ∀ 𝑓𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... sup ( 𝑔𝑀 ( 𝑔 supp 𝑍 ) , ℝ , < ) ) )
70 40 54 69 rspcedvd ( ( ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) ∧ ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ) ∧ ∀ 𝑓𝑀 𝑓 finSupp 𝑍 ) → ∃ 𝑚 ∈ ℕ0𝑓𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) )
71 70 exp31 ( ¬ ( ∅ = 𝑀 ∨ ∀ 𝑓𝑀 ( 𝑓 supp 𝑍 ) = ∅ ) → ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) → ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍 → ∃ 𝑚 ∈ ℕ0𝑓𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) ) ) )
72 16 71 pm2.61i ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) → ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍 → ∃ 𝑚 ∈ ℕ0𝑓𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) ) )