| Step | Hyp | Ref
| Expression |
| 1 | | nfv 1914 |
. . . 4
⊢
Ⅎ𝑓(𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) |
| 2 | | nfra1 3284 |
. . . . 5
⊢
Ⅎ𝑓∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 |
| 3 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑓 𝑈 ≠ ∅ |
| 4 | 2, 3 | nfan 1899 |
. . . 4
⊢
Ⅎ𝑓(∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅) |
| 5 | 1, 4 | nfan 1899 |
. . 3
⊢
Ⅎ𝑓((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) |
| 6 | | suppssdm 8202 |
. . . . . . . . . . 11
⊢ (𝑓 supp 𝑍) ⊆ dom 𝑓 |
| 7 | | ssel2 3978 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑓 ∈ 𝑀) → 𝑓 ∈ (𝑅 ↑m
ℕ0)) |
| 8 | | elmapfn 8905 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ (𝑅 ↑m ℕ0)
→ 𝑓 Fn
ℕ0) |
| 9 | | fndm 6671 |
. . . . . . . . . . . . 13
⊢ (𝑓 Fn ℕ0 →
dom 𝑓 =
ℕ0) |
| 10 | | eqimss 4042 |
. . . . . . . . . . . . 13
⊢ (dom
𝑓 = ℕ0
→ dom 𝑓 ⊆
ℕ0) |
| 11 | 7, 8, 9, 10 | 4syl 19 |
. . . . . . . . . . . 12
⊢ ((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑓 ∈ 𝑀) → dom 𝑓 ⊆
ℕ0) |
| 12 | 11 | 3ad2antl1 1186 |
. . . . . . . . . . 11
⊢ (((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ 𝑓 ∈ 𝑀) → dom 𝑓 ⊆
ℕ0) |
| 13 | 6, 12 | sstrid 3995 |
. . . . . . . . . 10
⊢ (((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ 𝑓 ∈ 𝑀) → (𝑓 supp 𝑍) ⊆
ℕ0) |
| 14 | 13 | sseld 3982 |
. . . . . . . . 9
⊢ (((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ 𝑓 ∈ 𝑀) → (𝑥 ∈ (𝑓 supp 𝑍) → 𝑥 ∈
ℕ0)) |
| 15 | 14 | adantlr 715 |
. . . . . . . 8
⊢ ((((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) → (𝑥 ∈ (𝑓 supp 𝑍) → 𝑥 ∈
ℕ0)) |
| 16 | 15 | imp 406 |
. . . . . . 7
⊢
(((((𝑀 ⊆
(𝑅 ↑m
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ (𝑓 supp 𝑍)) → 𝑥 ∈ ℕ0) |
| 17 | | fsuppmapnn0fiub.u |
. . . . . . . . . 10
⊢ 𝑈 = ∪ 𝑓 ∈ 𝑀 (𝑓 supp 𝑍) |
| 18 | | fsuppmapnn0fiub.s |
. . . . . . . . . 10
⊢ 𝑆 = sup(𝑈, ℝ, < ) |
| 19 | 17, 18 | fsuppmapnn0fiublem 14031 |
. . . . . . . . 9
⊢ ((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) → ((∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅) → 𝑆 ∈
ℕ0)) |
| 20 | 19 | imp 406 |
. . . . . . . 8
⊢ (((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) → 𝑆 ∈
ℕ0) |
| 21 | 20 | ad2antrr 726 |
. . . . . . 7
⊢
(((((𝑀 ⊆
(𝑅 ↑m
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ (𝑓 supp 𝑍)) → 𝑆 ∈
ℕ0) |
| 22 | 7, 8, 9 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑓 ∈ 𝑀) → dom 𝑓 = ℕ0) |
| 23 | 22 | ex 412 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ⊆ (𝑅 ↑m ℕ0)
→ (𝑓 ∈ 𝑀 → dom 𝑓 = ℕ0)) |
| 24 | 23 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) → (𝑓 ∈ 𝑀 → dom 𝑓 = ℕ0)) |
| 25 | 24 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) → (𝑓 ∈ 𝑀 → dom 𝑓 = ℕ0)) |
| 26 | 25 | imp 406 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) → dom 𝑓 = ℕ0) |
| 27 | | nn0ssre 12530 |
. . . . . . . . . . . . . . 15
⊢
ℕ0 ⊆ ℝ |
| 28 | 26, 27 | eqsstrdi 4028 |
. . . . . . . . . . . . . 14
⊢ ((((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) → dom 𝑓 ⊆ ℝ) |
| 29 | 6, 28 | sstrid 3995 |
. . . . . . . . . . . . 13
⊢ ((((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) → (𝑓 supp 𝑍) ⊆ ℝ) |
| 30 | 29 | ex 412 |
. . . . . . . . . . . 12
⊢ (((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) → (𝑓 ∈ 𝑀 → (𝑓 supp 𝑍) ⊆ ℝ)) |
| 31 | 5, 30 | ralrimi 3257 |
. . . . . . . . . . 11
⊢ (((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) → ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ ℝ) |
| 32 | 31 | ad2antrr 726 |
. . . . . . . . . 10
⊢
(((((𝑀 ⊆
(𝑅 ↑m
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ (𝑓 supp 𝑍)) → ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ ℝ) |
| 33 | | iunss 5045 |
. . . . . . . . . 10
⊢ (∪ 𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ ℝ ↔ ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ ℝ) |
| 34 | 32, 33 | sylibr 234 |
. . . . . . . . 9
⊢
(((((𝑀 ⊆
(𝑅 ↑m
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ (𝑓 supp 𝑍)) → ∪ 𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ ℝ) |
| 35 | 17, 34 | eqsstrid 4022 |
. . . . . . . 8
⊢
(((((𝑀 ⊆
(𝑅 ↑m
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ (𝑓 supp 𝑍)) → 𝑈 ⊆ ℝ) |
| 36 | | simp2 1138 |
. . . . . . . . . . . 12
⊢ ((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) → 𝑀 ∈ Fin) |
| 37 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 finSupp 𝑍 → 𝑓 finSupp 𝑍) |
| 38 | 37 | fsuppimpd 9409 |
. . . . . . . . . . . . . 14
⊢ (𝑓 finSupp 𝑍 → (𝑓 supp 𝑍) ∈ Fin) |
| 39 | 38 | ralimi 3083 |
. . . . . . . . . . . . 13
⊢
(∀𝑓 ∈
𝑀 𝑓 finSupp 𝑍 → ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ∈ Fin) |
| 40 | 39 | adantr 480 |
. . . . . . . . . . . 12
⊢
((∀𝑓 ∈
𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅) → ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ∈ Fin) |
| 41 | 36, 40 | anim12i 613 |
. . . . . . . . . . 11
⊢ (((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) → (𝑀 ∈ Fin ∧ ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ∈ Fin)) |
| 42 | 41 | ad2antrr 726 |
. . . . . . . . . 10
⊢
(((((𝑀 ⊆
(𝑅 ↑m
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ (𝑓 supp 𝑍)) → (𝑀 ∈ Fin ∧ ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ∈ Fin)) |
| 43 | | iunfi 9383 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ Fin ∧ ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ∈ Fin) → ∪ 𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ∈ Fin) |
| 44 | 42, 43 | syl 17 |
. . . . . . . . 9
⊢
(((((𝑀 ⊆
(𝑅 ↑m
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ (𝑓 supp 𝑍)) → ∪ 𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ∈ Fin) |
| 45 | 17, 44 | eqeltrid 2845 |
. . . . . . . 8
⊢
(((((𝑀 ⊆
(𝑅 ↑m
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ (𝑓 supp 𝑍)) → 𝑈 ∈ Fin) |
| 46 | | rspe 3249 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ 𝑀 ∧ 𝑥 ∈ (𝑓 supp 𝑍)) → ∃𝑓 ∈ 𝑀 𝑥 ∈ (𝑓 supp 𝑍)) |
| 47 | | eliun 4995 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ∪ 𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ↔ ∃𝑓 ∈ 𝑀 𝑥 ∈ (𝑓 supp 𝑍)) |
| 48 | 46, 47 | sylibr 234 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ 𝑀 ∧ 𝑥 ∈ (𝑓 supp 𝑍)) → 𝑥 ∈ ∪
𝑓 ∈ 𝑀 (𝑓 supp 𝑍)) |
| 49 | 48, 17 | eleqtrrdi 2852 |
. . . . . . . . 9
⊢ ((𝑓 ∈ 𝑀 ∧ 𝑥 ∈ (𝑓 supp 𝑍)) → 𝑥 ∈ 𝑈) |
| 50 | 49 | adantll 714 |
. . . . . . . 8
⊢
(((((𝑀 ⊆
(𝑅 ↑m
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ (𝑓 supp 𝑍)) → 𝑥 ∈ 𝑈) |
| 51 | 18 | a1i 11 |
. . . . . . . 8
⊢
(((((𝑀 ⊆
(𝑅 ↑m
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ (𝑓 supp 𝑍)) → 𝑆 = sup(𝑈, ℝ, < )) |
| 52 | 35, 45, 50, 51 | supfirege 12255 |
. . . . . . 7
⊢
(((((𝑀 ⊆
(𝑅 ↑m
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ (𝑓 supp 𝑍)) → 𝑥 ≤ 𝑆) |
| 53 | | elfz2nn0 13658 |
. . . . . . 7
⊢ (𝑥 ∈ (0...𝑆) ↔ (𝑥 ∈ ℕ0 ∧ 𝑆 ∈ ℕ0
∧ 𝑥 ≤ 𝑆)) |
| 54 | 16, 21, 52, 53 | syl3anbrc 1344 |
. . . . . 6
⊢
(((((𝑀 ⊆
(𝑅 ↑m
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ (𝑓 supp 𝑍)) → 𝑥 ∈ (0...𝑆)) |
| 55 | 54 | ex 412 |
. . . . 5
⊢ ((((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) → (𝑥 ∈ (𝑓 supp 𝑍) → 𝑥 ∈ (0...𝑆))) |
| 56 | 55 | ssrdv 3989 |
. . . 4
⊢ ((((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) ∧ 𝑓 ∈ 𝑀) → (𝑓 supp 𝑍) ⊆ (0...𝑆)) |
| 57 | 56 | ex 412 |
. . 3
⊢ (((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) → (𝑓 ∈ 𝑀 → (𝑓 supp 𝑍) ⊆ (0...𝑆))) |
| 58 | 5, 57 | ralrimi 3257 |
. 2
⊢ (((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅)) → ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...𝑆)) |
| 59 | 58 | ex 412 |
1
⊢ ((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) → ((∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅) → ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...𝑆))) |