Step | Hyp | Ref
| Expression |
1 | | frnnn0supp 12317 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐺:𝐼⟶ℕ0) → (𝐺 supp 0) = (◡𝐺 “ ℕ)) |
2 | 1 | 3ad2antr2 1187 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) → (𝐺 supp 0) = (◡𝐺 “ ℕ)) |
3 | | simpr2 1193 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) → 𝐺:𝐼⟶ℕ0) |
4 | | eldifi 4064 |
. . . . . 6
⊢ (𝑥 ∈ (𝐼 ∖ (◡𝐹 “ ℕ)) → 𝑥 ∈ 𝐼) |
5 | | simpr3 1194 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) → 𝐺 ∘r ≤ 𝐹) |
6 | 3 | ffnd 6619 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) → 𝐺 Fn 𝐼) |
7 | | psrbag.d |
. . . . . . . . . . . 12
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin} |
8 | 7 | psrbagfOLD 21150 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) → 𝐹:𝐼⟶ℕ0) |
9 | 8 | 3ad2antr1 1186 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) → 𝐹:𝐼⟶ℕ0) |
10 | 9 | ffnd 6619 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) → 𝐹 Fn 𝐼) |
11 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) → 𝐼 ∈ 𝑉) |
12 | | inidm 4155 |
. . . . . . . . 9
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
13 | | eqidd 2734 |
. . . . . . . . 9
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) ∧ 𝑥 ∈ 𝐼) → (𝐺‘𝑥) = (𝐺‘𝑥)) |
14 | | eqidd 2734 |
. . . . . . . . 9
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) = (𝐹‘𝑥)) |
15 | 6, 10, 11, 11, 12, 13, 14 | ofrfval 7563 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) → (𝐺 ∘r ≤ 𝐹 ↔ ∀𝑥 ∈ 𝐼 (𝐺‘𝑥) ≤ (𝐹‘𝑥))) |
16 | 5, 15 | mpbid 231 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) → ∀𝑥 ∈ 𝐼 (𝐺‘𝑥) ≤ (𝐹‘𝑥)) |
17 | 16 | r19.21bi 3228 |
. . . . . 6
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) ∧ 𝑥 ∈ 𝐼) → (𝐺‘𝑥) ≤ (𝐹‘𝑥)) |
18 | 4, 17 | sylan2 592 |
. . . . 5
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) ∧ 𝑥 ∈ (𝐼 ∖ (◡𝐹 “ ℕ))) → (𝐺‘𝑥) ≤ (𝐹‘𝑥)) |
19 | 11, 9 | jca 511 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) → (𝐼 ∈ 𝑉 ∧ 𝐹:𝐼⟶ℕ0)) |
20 | | frnnn0supp 12317 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹:𝐼⟶ℕ0) → (𝐹 supp 0) = (◡𝐹 “ ℕ)) |
21 | | eqimss 3979 |
. . . . . . 7
⊢ ((𝐹 supp 0) = (◡𝐹 “ ℕ) → (𝐹 supp 0) ⊆ (◡𝐹 “ ℕ)) |
22 | 19, 20, 21 | 3syl 18 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) → (𝐹 supp 0) ⊆ (◡𝐹 “ ℕ)) |
23 | | c0ex 10997 |
. . . . . . 7
⊢ 0 ∈
V |
24 | 23 | a1i 11 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) → 0 ∈
V) |
25 | 9, 22, 11, 24 | suppssr 8032 |
. . . . 5
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) ∧ 𝑥 ∈ (𝐼 ∖ (◡𝐹 “ ℕ))) → (𝐹‘𝑥) = 0) |
26 | 18, 25 | breqtrd 5103 |
. . . 4
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) ∧ 𝑥 ∈ (𝐼 ∖ (◡𝐹 “ ℕ))) → (𝐺‘𝑥) ≤ 0) |
27 | | ffvelcdm 6979 |
. . . . . 6
⊢ ((𝐺:𝐼⟶ℕ0 ∧ 𝑥 ∈ 𝐼) → (𝐺‘𝑥) ∈
ℕ0) |
28 | 3, 4, 27 | syl2an 595 |
. . . . 5
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) ∧ 𝑥 ∈ (𝐼 ∖ (◡𝐹 “ ℕ))) → (𝐺‘𝑥) ∈
ℕ0) |
29 | 28 | nn0ge0d 12324 |
. . . 4
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) ∧ 𝑥 ∈ (𝐼 ∖ (◡𝐹 “ ℕ))) → 0 ≤ (𝐺‘𝑥)) |
30 | 28 | nn0red 12322 |
. . . . 5
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) ∧ 𝑥 ∈ (𝐼 ∖ (◡𝐹 “ ℕ))) → (𝐺‘𝑥) ∈ ℝ) |
31 | | 0re 11005 |
. . . . 5
⊢ 0 ∈
ℝ |
32 | | letri3 11088 |
. . . . 5
⊢ (((𝐺‘𝑥) ∈ ℝ ∧ 0 ∈ ℝ)
→ ((𝐺‘𝑥) = 0 ↔ ((𝐺‘𝑥) ≤ 0 ∧ 0 ≤ (𝐺‘𝑥)))) |
33 | 30, 31, 32 | sylancl 585 |
. . . 4
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) ∧ 𝑥 ∈ (𝐼 ∖ (◡𝐹 “ ℕ))) → ((𝐺‘𝑥) = 0 ↔ ((𝐺‘𝑥) ≤ 0 ∧ 0 ≤ (𝐺‘𝑥)))) |
34 | 26, 29, 33 | mpbir2and 709 |
. . 3
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) ∧ 𝑥 ∈ (𝐼 ∖ (◡𝐹 “ ℕ))) → (𝐺‘𝑥) = 0) |
35 | 3, 34 | suppss 8030 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) → (𝐺 supp 0) ⊆ (◡𝐹 “ ℕ)) |
36 | 2, 35 | eqsstrrd 3962 |
1
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) → (◡𝐺 “ ℕ) ⊆ (◡𝐹 “ ℕ)) |