Step | Hyp | Ref
| Expression |
1 | | frnnn0supp 11226 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐺:𝐼⟶ℕ0) → (𝐺 supp 0) = (◡𝐺 “ ℕ)) |
2 | 1 | 3ad2antr2 1220 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → (𝐺 supp 0) = (◡𝐺 “ ℕ)) |
3 | | simpr2 1061 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → 𝐺:𝐼⟶ℕ0) |
4 | | eldifi 3694 |
. . . . . 6
⊢ (𝑥 ∈ (𝐼 ∖ (◡𝐹 “ ℕ)) → 𝑥 ∈ 𝐼) |
5 | | simpr3 1062 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → 𝐺 ∘𝑟
≤ 𝐹) |
6 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝐺:𝐼⟶ℕ0 → 𝐺 Fn 𝐼) |
7 | 3, 6 | syl 17 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → 𝐺 Fn 𝐼) |
8 | | psrbag.d |
. . . . . . . . . . . 12
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin} |
9 | 8 | psrbagf 19186 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) → 𝐹:𝐼⟶ℕ0) |
10 | 9 | 3ad2antr1 1219 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → 𝐹:𝐼⟶ℕ0) |
11 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝐹:𝐼⟶ℕ0 → 𝐹 Fn 𝐼) |
12 | 10, 11 | syl 17 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → 𝐹 Fn 𝐼) |
13 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → 𝐼 ∈ 𝑉) |
14 | | inidm 3784 |
. . . . . . . . 9
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
15 | | eqidd 2611 |
. . . . . . . . 9
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) ∧ 𝑥 ∈ 𝐼) → (𝐺‘𝑥) = (𝐺‘𝑥)) |
16 | | eqidd 2611 |
. . . . . . . . 9
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) = (𝐹‘𝑥)) |
17 | 7, 12, 13, 13, 14, 15, 16 | ofrfval 6803 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → (𝐺 ∘𝑟
≤ 𝐹 ↔ ∀𝑥 ∈ 𝐼 (𝐺‘𝑥) ≤ (𝐹‘𝑥))) |
18 | 5, 17 | mpbid 221 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) →
∀𝑥 ∈ 𝐼 (𝐺‘𝑥) ≤ (𝐹‘𝑥)) |
19 | 18 | r19.21bi 2916 |
. . . . . 6
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) ∧ 𝑥 ∈ 𝐼) → (𝐺‘𝑥) ≤ (𝐹‘𝑥)) |
20 | 4, 19 | sylan2 490 |
. . . . 5
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) ∧ 𝑥 ∈ (𝐼 ∖ (◡𝐹 “ ℕ))) → (𝐺‘𝑥) ≤ (𝐹‘𝑥)) |
21 | 13, 10 | jca 553 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → (𝐼 ∈ 𝑉 ∧ 𝐹:𝐼⟶ℕ0)) |
22 | | frnnn0supp 11226 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹:𝐼⟶ℕ0) → (𝐹 supp 0) = (◡𝐹 “ ℕ)) |
23 | | eqimss 3620 |
. . . . . . 7
⊢ ((𝐹 supp 0) = (◡𝐹 “ ℕ) → (𝐹 supp 0) ⊆ (◡𝐹 “ ℕ)) |
24 | 21, 22, 23 | 3syl 18 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → (𝐹 supp 0) ⊆ (◡𝐹 “ ℕ)) |
25 | | c0ex 9913 |
. . . . . . 7
⊢ 0 ∈
V |
26 | 25 | a1i 11 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → 0 ∈
V) |
27 | 10, 24, 13, 26 | suppssr 7213 |
. . . . 5
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) ∧ 𝑥 ∈ (𝐼 ∖ (◡𝐹 “ ℕ))) → (𝐹‘𝑥) = 0) |
28 | 20, 27 | breqtrd 4609 |
. . . 4
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) ∧ 𝑥 ∈ (𝐼 ∖ (◡𝐹 “ ℕ))) → (𝐺‘𝑥) ≤ 0) |
29 | | ffvelrn 6265 |
. . . . . 6
⊢ ((𝐺:𝐼⟶ℕ0 ∧ 𝑥 ∈ 𝐼) → (𝐺‘𝑥) ∈
ℕ0) |
30 | 3, 4, 29 | syl2an 493 |
. . . . 5
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) ∧ 𝑥 ∈ (𝐼 ∖ (◡𝐹 “ ℕ))) → (𝐺‘𝑥) ∈
ℕ0) |
31 | 30 | nn0ge0d 11231 |
. . . 4
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) ∧ 𝑥 ∈ (𝐼 ∖ (◡𝐹 “ ℕ))) → 0 ≤ (𝐺‘𝑥)) |
32 | 30 | nn0red 11229 |
. . . . 5
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) ∧ 𝑥 ∈ (𝐼 ∖ (◡𝐹 “ ℕ))) → (𝐺‘𝑥) ∈ ℝ) |
33 | | 0re 9919 |
. . . . 5
⊢ 0 ∈
ℝ |
34 | | letri3 10002 |
. . . . 5
⊢ (((𝐺‘𝑥) ∈ ℝ ∧ 0 ∈ ℝ)
→ ((𝐺‘𝑥) = 0 ↔ ((𝐺‘𝑥) ≤ 0 ∧ 0 ≤ (𝐺‘𝑥)))) |
35 | 32, 33, 34 | sylancl 693 |
. . . 4
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) ∧ 𝑥 ∈ (𝐼 ∖ (◡𝐹 “ ℕ))) → ((𝐺‘𝑥) = 0 ↔ ((𝐺‘𝑥) ≤ 0 ∧ 0 ≤ (𝐺‘𝑥)))) |
36 | 28, 31, 35 | mpbir2and 959 |
. . 3
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) ∧ 𝑥 ∈ (𝐼 ∖ (◡𝐹 “ ℕ))) → (𝐺‘𝑥) = 0) |
37 | 3, 36 | suppss 7212 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → (𝐺 supp 0) ⊆ (◡𝐹 “ ℕ)) |
38 | 2, 37 | eqsstr3d 3603 |
1
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → (◡𝐺 “ ℕ) ⊆ (◡𝐹 “ ℕ)) |