Step | Hyp | Ref
| Expression |
1 | | nfv 1830 |
. . . 4
⊢
Ⅎ𝑓(𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) |
2 | | nfra1 2925 |
. . . . 5
⊢
Ⅎ𝑓∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 |
3 | | nfv 1830 |
. . . . 5
⊢
Ⅎ𝑓 𝑈 ≠ ∅ |
4 | 2, 3 | nfan 1816 |
. . . 4
⊢
Ⅎ𝑓(∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅) |
5 | 1, 4 | nfan 1816 |
. . 3
⊢
Ⅎ𝑓((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) |
6 | | suppssdm 7195 |
. . . . . . . . . . 11
⊢ (𝑓 supp 𝑍) ⊆ dom 𝑓 |
7 | | ssel2 3563 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑓 ∈ 𝑀) → 𝑓 ∈ (𝑅 ↑𝑚
ℕ0)) |
8 | | elmapfn 7766 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ (𝑅 ↑𝑚
ℕ0) → 𝑓 Fn ℕ0) |
9 | | fndm 5904 |
. . . . . . . . . . . . . 14
⊢ (𝑓 Fn ℕ0 →
dom 𝑓 =
ℕ0) |
10 | | eqimss 3620 |
. . . . . . . . . . . . . 14
⊢ (dom
𝑓 = ℕ0
→ dom 𝑓 ⊆
ℕ0) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑓 Fn ℕ0 →
dom 𝑓 ⊆
ℕ0) |
12 | 7, 8, 11 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑓 ∈ 𝑀) → dom 𝑓 ⊆
ℕ0) |
13 | 12 | 3ad2antl1 1216 |
. . . . . . . . . . 11
⊢ (((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ 𝑓 ∈ 𝑀) → dom 𝑓 ⊆
ℕ0) |
14 | 6, 13 | syl5ss 3579 |
. . . . . . . . . 10
⊢ (((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ 𝑓 ∈ 𝑀) → (𝑓 supp 𝑍) ⊆
ℕ0) |
15 | 14 | sseld 3567 |
. . . . . . . . 9
⊢ (((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ 𝑓 ∈ 𝑀) → (𝑥 ∈ (𝑓 supp 𝑍) → 𝑥 ∈
ℕ0)) |
16 | 15 | adantlr 747 |
. . . . . . . 8
⊢ ((((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) → (𝑥 ∈ (𝑓 supp 𝑍) → 𝑥 ∈
ℕ0)) |
17 | 16 | imp 444 |
. . . . . . 7
⊢
(((((𝑀 ⊆
(𝑅
↑𝑚 ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ (𝑓 supp 𝑍)) → 𝑥 ∈ ℕ0) |
18 | | fsuppmapnn0fiub.u |
. . . . . . . . . 10
⊢ 𝑈 = ∪ 𝑓 ∈ 𝑀 (𝑓 supp 𝑍) |
19 | | fsuppmapnn0fiub.s |
. . . . . . . . . 10
⊢ 𝑆 = sup(𝑈, ℝ, < ) |
20 | 18, 19 | fsuppmapnn0fiublem 12651 |
. . . . . . . . 9
⊢ ((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) → ((∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅) → 𝑆 ∈
ℕ0)) |
21 | 20 | imp 444 |
. . . . . . . 8
⊢ (((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) → 𝑆 ∈
ℕ0) |
22 | 21 | ad2antrr 758 |
. . . . . . 7
⊢
(((((𝑀 ⊆
(𝑅
↑𝑚 ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ (𝑓 supp 𝑍)) → 𝑆 ∈
ℕ0) |
23 | 7, 8, 9 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑓 ∈ 𝑀) → dom 𝑓 = ℕ0) |
24 | 23 | ex 449 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) → (𝑓 ∈ 𝑀 → dom 𝑓 = ℕ0)) |
25 | 24 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) → (𝑓 ∈ 𝑀 → dom 𝑓 = ℕ0)) |
26 | 25 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) → (𝑓 ∈ 𝑀 → dom 𝑓 = ℕ0)) |
27 | 26 | imp 444 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) → dom 𝑓 = ℕ0) |
28 | | nn0ssre 11173 |
. . . . . . . . . . . . . . 15
⊢
ℕ0 ⊆ ℝ |
29 | 27, 28 | syl6eqss 3618 |
. . . . . . . . . . . . . 14
⊢ ((((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) → dom 𝑓 ⊆ ℝ) |
30 | 6, 29 | syl5ss 3579 |
. . . . . . . . . . . . 13
⊢ ((((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) → (𝑓 supp 𝑍) ⊆ ℝ) |
31 | 30 | ex 449 |
. . . . . . . . . . . 12
⊢ (((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) → (𝑓 ∈ 𝑀 → (𝑓 supp 𝑍) ⊆ ℝ)) |
32 | 5, 31 | ralrimi 2940 |
. . . . . . . . . . 11
⊢ (((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) → ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ ℝ) |
33 | 32 | ad2antrr 758 |
. . . . . . . . . 10
⊢
(((((𝑀 ⊆
(𝑅
↑𝑚 ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ (𝑓 supp 𝑍)) → ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ ℝ) |
34 | | iunss 4497 |
. . . . . . . . . 10
⊢ (∪ 𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ ℝ ↔ ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ ℝ) |
35 | 33, 34 | sylibr 223 |
. . . . . . . . 9
⊢
(((((𝑀 ⊆
(𝑅
↑𝑚 ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ (𝑓 supp 𝑍)) → ∪ 𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ ℝ) |
36 | 18, 35 | syl5eqss 3612 |
. . . . . . . 8
⊢
(((((𝑀 ⊆
(𝑅
↑𝑚 ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ (𝑓 supp 𝑍)) → 𝑈 ⊆ ℝ) |
37 | | simp2 1055 |
. . . . . . . . . . . 12
⊢ ((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) → 𝑀 ∈ Fin) |
38 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 finSupp 𝑍 → 𝑓 finSupp 𝑍) |
39 | 38 | fsuppimpd 8165 |
. . . . . . . . . . . . . 14
⊢ (𝑓 finSupp 𝑍 → (𝑓 supp 𝑍) ∈ Fin) |
40 | 39 | ralimi 2936 |
. . . . . . . . . . . . 13
⊢
(∀𝑓 ∈
𝑀 𝑓 finSupp 𝑍 → ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ∈ Fin) |
41 | 40 | adantr 480 |
. . . . . . . . . . . 12
⊢
((∀𝑓 ∈
𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅) → ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ∈ Fin) |
42 | 37, 41 | anim12i 588 |
. . . . . . . . . . 11
⊢ (((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) → (𝑀 ∈ Fin ∧ ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ∈ Fin)) |
43 | 42 | ad2antrr 758 |
. . . . . . . . . 10
⊢
(((((𝑀 ⊆
(𝑅
↑𝑚 ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ (𝑓 supp 𝑍)) → (𝑀 ∈ Fin ∧ ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ∈ Fin)) |
44 | | iunfi 8137 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ Fin ∧ ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ∈ Fin) → ∪ 𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ∈ Fin) |
45 | 43, 44 | syl 17 |
. . . . . . . . 9
⊢
(((((𝑀 ⊆
(𝑅
↑𝑚 ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ (𝑓 supp 𝑍)) → ∪ 𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ∈ Fin) |
46 | 18, 45 | syl5eqel 2692 |
. . . . . . . 8
⊢
(((((𝑀 ⊆
(𝑅
↑𝑚 ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ (𝑓 supp 𝑍)) → 𝑈 ∈ Fin) |
47 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) → 𝑓 ∈ 𝑀) |
48 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = 𝑓 → (𝑔 supp 𝑍) = (𝑓 supp 𝑍)) |
49 | 48 | eleq2d 2673 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝑓 → (𝑥 ∈ (𝑔 supp 𝑍) ↔ 𝑥 ∈ (𝑓 supp 𝑍))) |
50 | 49 | adantl 481 |
. . . . . . . . . . . 12
⊢
(((((𝑀 ⊆
(𝑅
↑𝑚 ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) ∧ 𝑔 = 𝑓) → (𝑥 ∈ (𝑔 supp 𝑍) ↔ 𝑥 ∈ (𝑓 supp 𝑍))) |
51 | 47, 50 | rspcedv 3286 |
. . . . . . . . . . 11
⊢ ((((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) → (𝑥 ∈ (𝑓 supp 𝑍) → ∃𝑔 ∈ 𝑀 𝑥 ∈ (𝑔 supp 𝑍))) |
52 | 51 | imp 444 |
. . . . . . . . . 10
⊢
(((((𝑀 ⊆
(𝑅
↑𝑚 ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ (𝑓 supp 𝑍)) → ∃𝑔 ∈ 𝑀 𝑥 ∈ (𝑔 supp 𝑍)) |
53 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑔 → (𝑓 supp 𝑍) = (𝑔 supp 𝑍)) |
54 | 53 | eleq2d 2673 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑔 → (𝑥 ∈ (𝑓 supp 𝑍) ↔ 𝑥 ∈ (𝑔 supp 𝑍))) |
55 | 54 | cbvrexv 3148 |
. . . . . . . . . 10
⊢
(∃𝑓 ∈
𝑀 𝑥 ∈ (𝑓 supp 𝑍) ↔ ∃𝑔 ∈ 𝑀 𝑥 ∈ (𝑔 supp 𝑍)) |
56 | 52, 55 | sylibr 223 |
. . . . . . . . 9
⊢
(((((𝑀 ⊆
(𝑅
↑𝑚 ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ (𝑓 supp 𝑍)) → ∃𝑓 ∈ 𝑀 𝑥 ∈ (𝑓 supp 𝑍)) |
57 | 18 | eleq2i 2680 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑈 ↔ 𝑥 ∈ ∪
𝑓 ∈ 𝑀 (𝑓 supp 𝑍)) |
58 | | eliun 4460 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ∪ 𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ↔ ∃𝑓 ∈ 𝑀 𝑥 ∈ (𝑓 supp 𝑍)) |
59 | 57, 58 | bitri 263 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑈 ↔ ∃𝑓 ∈ 𝑀 𝑥 ∈ (𝑓 supp 𝑍)) |
60 | 56, 59 | sylibr 223 |
. . . . . . . 8
⊢
(((((𝑀 ⊆
(𝑅
↑𝑚 ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ (𝑓 supp 𝑍)) → 𝑥 ∈ 𝑈) |
61 | 19 | a1i 11 |
. . . . . . . 8
⊢
(((((𝑀 ⊆
(𝑅
↑𝑚 ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ (𝑓 supp 𝑍)) → 𝑆 = sup(𝑈, ℝ, < )) |
62 | 36, 46, 60, 61 | supfirege 10886 |
. . . . . . 7
⊢
(((((𝑀 ⊆
(𝑅
↑𝑚 ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ (𝑓 supp 𝑍)) → 𝑥 ≤ 𝑆) |
63 | | elfz2nn0 12300 |
. . . . . . 7
⊢ (𝑥 ∈ (0...𝑆) ↔ (𝑥 ∈ ℕ0 ∧ 𝑆 ∈ ℕ0
∧ 𝑥 ≤ 𝑆)) |
64 | 17, 22, 62, 63 | syl3anbrc 1239 |
. . . . . 6
⊢
(((((𝑀 ⊆
(𝑅
↑𝑚 ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ (𝑓 supp 𝑍)) → 𝑥 ∈ (0...𝑆)) |
65 | 64 | ex 449 |
. . . . 5
⊢ ((((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) → (𝑥 ∈ (𝑓 supp 𝑍) → 𝑥 ∈ (0...𝑆))) |
66 | 65 | ssrdv 3574 |
. . . 4
⊢ ((((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) → (𝑓 supp 𝑍) ⊆ (0...𝑆)) |
67 | 66 | ex 449 |
. . 3
⊢ (((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) → (𝑓 ∈ 𝑀 → (𝑓 supp 𝑍) ⊆ (0...𝑆))) |
68 | 5, 67 | ralrimi 2940 |
. 2
⊢ (((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) → ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...𝑆)) |
69 | 68 | ex 449 |
1
⊢ ((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) → ((∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅) → ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...𝑆))) |