Step | Hyp | Ref
| Expression |
1 | | frnnn0supp 12035 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐺:𝐼⟶ℕ0) → (𝐺 supp 0) = (◡𝐺 “ ℕ)) |
2 | 1 | 3ad2antr2 1190 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) → (𝐺 supp 0) = (◡𝐺 “ ℕ)) |
3 | | simpr2 1196 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) → 𝐺:𝐼⟶ℕ0) |
4 | | eldifi 4018 |
. . . . . 6
⊢ (𝑥 ∈ (𝐼 ∖ (◡𝐹 “ ℕ)) → 𝑥 ∈ 𝐼) |
5 | | simpr3 1197 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) → 𝐺 ∘r ≤ 𝐹) |
6 | 3 | ffnd 6506 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) → 𝐺 Fn 𝐼) |
7 | | psrbag.d |
. . . . . . . . . . . 12
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin} |
8 | 7 | psrbagfOLD 20735 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) → 𝐹:𝐼⟶ℕ0) |
9 | 8 | 3ad2antr1 1189 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) → 𝐹:𝐼⟶ℕ0) |
10 | 9 | ffnd 6506 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) → 𝐹 Fn 𝐼) |
11 | | simpl 486 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) → 𝐼 ∈ 𝑉) |
12 | | inidm 4110 |
. . . . . . . . 9
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
13 | | eqidd 2740 |
. . . . . . . . 9
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) ∧ 𝑥 ∈ 𝐼) → (𝐺‘𝑥) = (𝐺‘𝑥)) |
14 | | eqidd 2740 |
. . . . . . . . 9
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) = (𝐹‘𝑥)) |
15 | 6, 10, 11, 11, 12, 13, 14 | ofrfval 7437 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) → (𝐺 ∘r ≤ 𝐹 ↔ ∀𝑥 ∈ 𝐼 (𝐺‘𝑥) ≤ (𝐹‘𝑥))) |
16 | 5, 15 | mpbid 235 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) → ∀𝑥 ∈ 𝐼 (𝐺‘𝑥) ≤ (𝐹‘𝑥)) |
17 | 16 | r19.21bi 3122 |
. . . . . 6
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) ∧ 𝑥 ∈ 𝐼) → (𝐺‘𝑥) ≤ (𝐹‘𝑥)) |
18 | 4, 17 | sylan2 596 |
. . . . 5
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) ∧ 𝑥 ∈ (𝐼 ∖ (◡𝐹 “ ℕ))) → (𝐺‘𝑥) ≤ (𝐹‘𝑥)) |
19 | 11, 9 | jca 515 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) → (𝐼 ∈ 𝑉 ∧ 𝐹:𝐼⟶ℕ0)) |
20 | | frnnn0supp 12035 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹:𝐼⟶ℕ0) → (𝐹 supp 0) = (◡𝐹 “ ℕ)) |
21 | | eqimss 3934 |
. . . . . . 7
⊢ ((𝐹 supp 0) = (◡𝐹 “ ℕ) → (𝐹 supp 0) ⊆ (◡𝐹 “ ℕ)) |
22 | 19, 20, 21 | 3syl 18 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) → (𝐹 supp 0) ⊆ (◡𝐹 “ ℕ)) |
23 | | c0ex 10716 |
. . . . . . 7
⊢ 0 ∈
V |
24 | 23 | a1i 11 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) → 0 ∈
V) |
25 | 9, 22, 11, 24 | suppssr 7894 |
. . . . 5
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) ∧ 𝑥 ∈ (𝐼 ∖ (◡𝐹 “ ℕ))) → (𝐹‘𝑥) = 0) |
26 | 18, 25 | breqtrd 5057 |
. . . 4
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) ∧ 𝑥 ∈ (𝐼 ∖ (◡𝐹 “ ℕ))) → (𝐺‘𝑥) ≤ 0) |
27 | | ffvelrn 6862 |
. . . . . 6
⊢ ((𝐺:𝐼⟶ℕ0 ∧ 𝑥 ∈ 𝐼) → (𝐺‘𝑥) ∈
ℕ0) |
28 | 3, 4, 27 | syl2an 599 |
. . . . 5
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) ∧ 𝑥 ∈ (𝐼 ∖ (◡𝐹 “ ℕ))) → (𝐺‘𝑥) ∈
ℕ0) |
29 | 28 | nn0ge0d 12042 |
. . . 4
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) ∧ 𝑥 ∈ (𝐼 ∖ (◡𝐹 “ ℕ))) → 0 ≤ (𝐺‘𝑥)) |
30 | 28 | nn0red 12040 |
. . . . 5
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) ∧ 𝑥 ∈ (𝐼 ∖ (◡𝐹 “ ℕ))) → (𝐺‘𝑥) ∈ ℝ) |
31 | | 0re 10724 |
. . . . 5
⊢ 0 ∈
ℝ |
32 | | letri3 10807 |
. . . . 5
⊢ (((𝐺‘𝑥) ∈ ℝ ∧ 0 ∈ ℝ)
→ ((𝐺‘𝑥) = 0 ↔ ((𝐺‘𝑥) ≤ 0 ∧ 0 ≤ (𝐺‘𝑥)))) |
33 | 30, 31, 32 | sylancl 589 |
. . . 4
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) ∧ 𝑥 ∈ (𝐼 ∖ (◡𝐹 “ ℕ))) → ((𝐺‘𝑥) = 0 ↔ ((𝐺‘𝑥) ≤ 0 ∧ 0 ≤ (𝐺‘𝑥)))) |
34 | 26, 29, 33 | mpbir2and 713 |
. . 3
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) ∧ 𝑥 ∈ (𝐼 ∖ (◡𝐹 “ ℕ))) → (𝐺‘𝑥) = 0) |
35 | 3, 34 | suppss 7892 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) → (𝐺 supp 0) ⊆ (◡𝐹 “ ℕ)) |
36 | 2, 35 | eqsstrrd 3917 |
1
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘r ≤ 𝐹)) → (◡𝐺 “ ℕ) ⊆ (◡𝐹 “ ℕ)) |