| Step | Hyp | Ref
| Expression |
| 1 | | 0nn0 12541 |
. . . . 5
⊢ 0 ∈
ℕ0 |
| 2 | 1 | a1i 11 |
. . . 4
⊢ ((∅
= 𝑀 ∨ ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅) → 0 ∈
ℕ0) |
| 3 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑚 = 0 → (0...𝑚) = (0...0)) |
| 4 | 3 | sseq2d 4016 |
. . . . . 6
⊢ (𝑚 = 0 → ((𝑓 supp 𝑍) ⊆ (0...𝑚) ↔ (𝑓 supp 𝑍) ⊆ (0...0))) |
| 5 | 4 | ralbidv 3178 |
. . . . 5
⊢ (𝑚 = 0 → (∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...𝑚) ↔ ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...0))) |
| 6 | 5 | adantl 481 |
. . . 4
⊢
(((∅ = 𝑀 ∨
∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅) ∧ 𝑚 = 0) → (∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...𝑚) ↔ ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...0))) |
| 7 | | ral0 4513 |
. . . . . 6
⊢
∀𝑓 ∈
∅ (𝑓 supp 𝑍) ⊆
(0...0) |
| 8 | | raleq 3323 |
. . . . . 6
⊢ (∅
= 𝑀 → (∀𝑓 ∈ ∅ (𝑓 supp 𝑍) ⊆ (0...0) ↔ ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...0))) |
| 9 | 7, 8 | mpbii 233 |
. . . . 5
⊢ (∅
= 𝑀 → ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...0)) |
| 10 | | 0ss 4400 |
. . . . . . 7
⊢ ∅
⊆ (0...0) |
| 11 | | sseq1 4009 |
. . . . . . 7
⊢ ((𝑓 supp 𝑍) = ∅ → ((𝑓 supp 𝑍) ⊆ (0...0) ↔ ∅ ⊆
(0...0))) |
| 12 | 10, 11 | mpbiri 258 |
. . . . . 6
⊢ ((𝑓 supp 𝑍) = ∅ → (𝑓 supp 𝑍) ⊆ (0...0)) |
| 13 | 12 | ralimi 3083 |
. . . . 5
⊢
(∀𝑓 ∈
𝑀 (𝑓 supp 𝑍) = ∅ → ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...0)) |
| 14 | 9, 13 | jaoi 858 |
. . . 4
⊢ ((∅
= 𝑀 ∨ ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅) → ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...0)) |
| 15 | 2, 6, 14 | rspcedvd 3624 |
. . 3
⊢ ((∅
= 𝑀 ∨ ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅) → ∃𝑚 ∈ ℕ0
∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...𝑚)) |
| 16 | 15 | 2a1d 26 |
. 2
⊢ ((∅
= 𝑀 ∨ ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅) → ((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) → (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 → ∃𝑚 ∈ ℕ0 ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...𝑚)))) |
| 17 | | simplr 769 |
. . . . 5
⊢ (((¬
(∅ = 𝑀 ∨
∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅) ∧ (𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉)) ∧ ∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍) → (𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉)) |
| 18 | | simpr 484 |
. . . . . 6
⊢ (((¬
(∅ = 𝑀 ∨
∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅) ∧ (𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉)) ∧ ∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍) → ∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍) |
| 19 | | ioran 986 |
. . . . . . . . . 10
⊢ (¬
(∅ = 𝑀 ∨
∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅) ↔ (¬ ∅ = 𝑀 ∧ ¬ ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅)) |
| 20 | | oveq1 7438 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝑔 → (𝑓 supp 𝑍) = (𝑔 supp 𝑍)) |
| 21 | 20 | eqeq1d 2739 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝑔 → ((𝑓 supp 𝑍) = ∅ ↔ (𝑔 supp 𝑍) = ∅)) |
| 22 | 21 | cbvralvw 3237 |
. . . . . . . . . . . 12
⊢
(∀𝑓 ∈
𝑀 (𝑓 supp 𝑍) = ∅ ↔ ∀𝑔 ∈ 𝑀 (𝑔 supp 𝑍) = ∅) |
| 23 | 22 | notbii 320 |
. . . . . . . . . . 11
⊢ (¬
∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅ ↔ ¬ ∀𝑔 ∈ 𝑀 (𝑔 supp 𝑍) = ∅) |
| 24 | 23 | anbi2i 623 |
. . . . . . . . . 10
⊢ ((¬
∅ = 𝑀 ∧ ¬
∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅) ↔ (¬ ∅ = 𝑀 ∧ ¬ ∀𝑔 ∈ 𝑀 (𝑔 supp 𝑍) = ∅)) |
| 25 | 19, 24 | bitri 275 |
. . . . . . . . 9
⊢ (¬
(∅ = 𝑀 ∨
∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅) ↔ (¬ ∅ = 𝑀 ∧ ¬ ∀𝑔 ∈ 𝑀 (𝑔 supp 𝑍) = ∅)) |
| 26 | | rexnal 3100 |
. . . . . . . . . 10
⊢
(∃𝑔 ∈
𝑀 ¬ (𝑔 supp 𝑍) = ∅ ↔ ¬ ∀𝑔 ∈ 𝑀 (𝑔 supp 𝑍) = ∅) |
| 27 | | df-ne 2941 |
. . . . . . . . . . . 12
⊢ ((𝑔 supp 𝑍) ≠ ∅ ↔ ¬ (𝑔 supp 𝑍) = ∅) |
| 28 | 27 | bicomi 224 |
. . . . . . . . . . 11
⊢ (¬
(𝑔 supp 𝑍) = ∅ ↔ (𝑔 supp 𝑍) ≠ ∅) |
| 29 | 28 | rexbii 3094 |
. . . . . . . . . 10
⊢
(∃𝑔 ∈
𝑀 ¬ (𝑔 supp 𝑍) = ∅ ↔ ∃𝑔 ∈ 𝑀 (𝑔 supp 𝑍) ≠ ∅) |
| 30 | 26, 29 | sylbb1 237 |
. . . . . . . . 9
⊢ (¬
∀𝑔 ∈ 𝑀 (𝑔 supp 𝑍) = ∅ → ∃𝑔 ∈ 𝑀 (𝑔 supp 𝑍) ≠ ∅) |
| 31 | 25, 30 | simplbiim 504 |
. . . . . . . 8
⊢ (¬
(∅ = 𝑀 ∨
∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅) → ∃𝑔 ∈ 𝑀 (𝑔 supp 𝑍) ≠ ∅) |
| 32 | 31 | ad2antrr 726 |
. . . . . . 7
⊢ (((¬
(∅ = 𝑀 ∨
∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅) ∧ (𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉)) ∧ ∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍) → ∃𝑔 ∈ 𝑀 (𝑔 supp 𝑍) ≠ ∅) |
| 33 | | iunn0 5067 |
. . . . . . 7
⊢
(∃𝑔 ∈
𝑀 (𝑔 supp 𝑍) ≠ ∅ ↔ ∪ 𝑔 ∈ 𝑀 (𝑔 supp 𝑍) ≠ ∅) |
| 34 | 32, 33 | sylib 218 |
. . . . . 6
⊢ (((¬
(∅ = 𝑀 ∨
∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅) ∧ (𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉)) ∧ ∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍) → ∪
𝑔 ∈ 𝑀 (𝑔 supp 𝑍) ≠ ∅) |
| 35 | 18, 34 | jca 511 |
. . . . 5
⊢ (((¬
(∅ = 𝑀 ∨
∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅) ∧ (𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉)) ∧ ∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍) → (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ ∪
𝑔 ∈ 𝑀 (𝑔 supp 𝑍) ≠ ∅)) |
| 36 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑔 = 𝑓 → (𝑔 supp 𝑍) = (𝑓 supp 𝑍)) |
| 37 | 36 | cbviunv 5040 |
. . . . . 6
⊢ ∪ 𝑔 ∈ 𝑀 (𝑔 supp 𝑍) = ∪
𝑓 ∈ 𝑀 (𝑓 supp 𝑍) |
| 38 | | eqid 2737 |
. . . . . 6
⊢
sup(∪ 𝑔 ∈ 𝑀 (𝑔 supp 𝑍), ℝ, < ) = sup(∪ 𝑔 ∈ 𝑀 (𝑔 supp 𝑍), ℝ, < ) |
| 39 | 37, 38 | fsuppmapnn0fiublem 14031 |
. . . . 5
⊢ ((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) → ((∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ ∪
𝑔 ∈ 𝑀 (𝑔 supp 𝑍) ≠ ∅) → sup(∪ 𝑔 ∈ 𝑀 (𝑔 supp 𝑍), ℝ, < ) ∈
ℕ0)) |
| 40 | 17, 35, 39 | sylc 65 |
. . . 4
⊢ (((¬
(∅ = 𝑀 ∨
∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅) ∧ (𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉)) ∧ ∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍) → sup(∪ 𝑔 ∈ 𝑀 (𝑔 supp 𝑍), ℝ, < ) ∈
ℕ0) |
| 41 | | nfv 1914 |
. . . . . . . . . 10
⊢
Ⅎ𝑓∅ =
𝑀 |
| 42 | | nfra1 3284 |
. . . . . . . . . 10
⊢
Ⅎ𝑓∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅ |
| 43 | 41, 42 | nfor 1904 |
. . . . . . . . 9
⊢
Ⅎ𝑓(∅ =
𝑀 ∨ ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅) |
| 44 | 43 | nfn 1857 |
. . . . . . . 8
⊢
Ⅎ𝑓 ¬
(∅ = 𝑀 ∨
∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅) |
| 45 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑓(𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) |
| 46 | 44, 45 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑓(¬
(∅ = 𝑀 ∨
∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅) ∧ (𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉)) |
| 47 | | nfra1 3284 |
. . . . . . 7
⊢
Ⅎ𝑓∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 |
| 48 | 46, 47 | nfan 1899 |
. . . . . 6
⊢
Ⅎ𝑓((¬
(∅ = 𝑀 ∨
∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅) ∧ (𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉)) ∧ ∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍) |
| 49 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑓 𝑚 = sup(∪ 𝑔 ∈ 𝑀 (𝑔 supp 𝑍), ℝ, < ) |
| 50 | 48, 49 | nfan 1899 |
. . . . 5
⊢
Ⅎ𝑓(((¬
(∅ = 𝑀 ∨
∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅) ∧ (𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉)) ∧ ∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍) ∧ 𝑚 = sup(∪
𝑔 ∈ 𝑀 (𝑔 supp 𝑍), ℝ, < )) |
| 51 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑚 = sup(∪ 𝑔 ∈ 𝑀 (𝑔 supp 𝑍), ℝ, < ) → (0...𝑚) = (0...sup(∪ 𝑔 ∈ 𝑀 (𝑔 supp 𝑍), ℝ, < ))) |
| 52 | 51 | sseq2d 4016 |
. . . . . 6
⊢ (𝑚 = sup(∪ 𝑔 ∈ 𝑀 (𝑔 supp 𝑍), ℝ, < ) → ((𝑓 supp 𝑍) ⊆ (0...𝑚) ↔ (𝑓 supp 𝑍) ⊆ (0...sup(∪ 𝑔 ∈ 𝑀 (𝑔 supp 𝑍), ℝ, < )))) |
| 53 | 52 | adantl 481 |
. . . . 5
⊢ ((((¬
(∅ = 𝑀 ∨
∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅) ∧ (𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉)) ∧ ∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍) ∧ 𝑚 = sup(∪
𝑔 ∈ 𝑀 (𝑔 supp 𝑍), ℝ, < )) → ((𝑓 supp 𝑍) ⊆ (0...𝑚) ↔ (𝑓 supp 𝑍) ⊆ (0...sup(∪ 𝑔 ∈ 𝑀 (𝑔 supp 𝑍), ℝ, < )))) |
| 54 | 50, 53 | ralbid 3273 |
. . . 4
⊢ ((((¬
(∅ = 𝑀 ∨
∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅) ∧ (𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉)) ∧ ∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍) ∧ 𝑚 = sup(∪
𝑔 ∈ 𝑀 (𝑔 supp 𝑍), ℝ, < )) → (∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...𝑚) ↔ ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...sup(∪ 𝑔 ∈ 𝑀 (𝑔 supp 𝑍), ℝ, < )))) |
| 55 | | rexnal 3100 |
. . . . . . . . . 10
⊢
(∃𝑓 ∈
𝑀 ¬ (𝑓 supp 𝑍) = ∅ ↔ ¬ ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅) |
| 56 | | df-ne 2941 |
. . . . . . . . . . . 12
⊢ ((𝑓 supp 𝑍) ≠ ∅ ↔ ¬ (𝑓 supp 𝑍) = ∅) |
| 57 | 56 | bicomi 224 |
. . . . . . . . . . 11
⊢ (¬
(𝑓 supp 𝑍) = ∅ ↔ (𝑓 supp 𝑍) ≠ ∅) |
| 58 | 57 | rexbii 3094 |
. . . . . . . . . 10
⊢
(∃𝑓 ∈
𝑀 ¬ (𝑓 supp 𝑍) = ∅ ↔ ∃𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ≠ ∅) |
| 59 | 55, 58 | sylbb1 237 |
. . . . . . . . 9
⊢ (¬
∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅ → ∃𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ≠ ∅) |
| 60 | 19, 59 | simplbiim 504 |
. . . . . . . 8
⊢ (¬
(∅ = 𝑀 ∨
∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅) → ∃𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ≠ ∅) |
| 61 | 60 | ad2antrr 726 |
. . . . . . 7
⊢ (((¬
(∅ = 𝑀 ∨
∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅) ∧ (𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉)) ∧ ∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍) → ∃𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ≠ ∅) |
| 62 | | iunn0 5067 |
. . . . . . . 8
⊢
(∃𝑓 ∈
𝑀 (𝑓 supp 𝑍) ≠ ∅ ↔ ∪ 𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ≠ ∅) |
| 63 | 20 | cbviunv 5040 |
. . . . . . . . 9
⊢ ∪ 𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∪
𝑔 ∈ 𝑀 (𝑔 supp 𝑍) |
| 64 | 63 | neeq1i 3005 |
. . . . . . . 8
⊢ (∪ 𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ≠ ∅ ↔ ∪ 𝑔 ∈ 𝑀 (𝑔 supp 𝑍) ≠ ∅) |
| 65 | 62, 64 | bitri 275 |
. . . . . . 7
⊢
(∃𝑓 ∈
𝑀 (𝑓 supp 𝑍) ≠ ∅ ↔ ∪ 𝑔 ∈ 𝑀 (𝑔 supp 𝑍) ≠ ∅) |
| 66 | 61, 65 | sylib 218 |
. . . . . 6
⊢ (((¬
(∅ = 𝑀 ∨
∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅) ∧ (𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉)) ∧ ∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍) → ∪
𝑔 ∈ 𝑀 (𝑔 supp 𝑍) ≠ ∅) |
| 67 | 18, 66 | jca 511 |
. . . . 5
⊢ (((¬
(∅ = 𝑀 ∨
∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅) ∧ (𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉)) ∧ ∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍) → (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ ∪
𝑔 ∈ 𝑀 (𝑔 supp 𝑍) ≠ ∅)) |
| 68 | 37, 38 | fsuppmapnn0fiub 14032 |
. . . . 5
⊢ ((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) → ((∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ ∪
𝑔 ∈ 𝑀 (𝑔 supp 𝑍) ≠ ∅) → ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...sup(∪ 𝑔 ∈ 𝑀 (𝑔 supp 𝑍), ℝ, < )))) |
| 69 | 17, 67, 68 | sylc 65 |
. . . 4
⊢ (((¬
(∅ = 𝑀 ∨
∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅) ∧ (𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉)) ∧ ∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍) → ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...sup(∪ 𝑔 ∈ 𝑀 (𝑔 supp 𝑍), ℝ, < ))) |
| 70 | 40, 54, 69 | rspcedvd 3624 |
. . 3
⊢ (((¬
(∅ = 𝑀 ∨
∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅) ∧ (𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉)) ∧ ∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍) → ∃𝑚 ∈ ℕ0 ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...𝑚)) |
| 71 | 70 | exp31 419 |
. 2
⊢ (¬
(∅ = 𝑀 ∨
∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) = ∅) → ((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) → (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 → ∃𝑚 ∈ ℕ0 ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...𝑚)))) |
| 72 | 16, 71 | pm2.61i 182 |
1
⊢ ((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) → (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 → ∃𝑚 ∈ ℕ0 ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...𝑚))) |