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 ... 𝑚 ) ) ) |