Step | Hyp | Ref
| Expression |
1 | | simpr1 1067 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → 𝐹 ∈ 𝐷) |
2 | | psrbag.d |
. . . . . . . . . 10
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin} |
3 | 2 | psrbag 19364 |
. . . . . . . . 9
⊢ (𝐼 ∈ 𝑉 → (𝐹 ∈ 𝐷 ↔ (𝐹:𝐼⟶ℕ0 ∧ (◡𝐹 “ ℕ) ∈
Fin))) |
4 | 3 | adantr 481 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → (𝐹 ∈ 𝐷 ↔ (𝐹:𝐼⟶ℕ0 ∧ (◡𝐹 “ ℕ) ∈
Fin))) |
5 | 1, 4 | mpbid 222 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → (𝐹:𝐼⟶ℕ0 ∧ (◡𝐹 “ ℕ) ∈
Fin)) |
6 | 5 | simpld 475 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → 𝐹:𝐼⟶ℕ0) |
7 | | ffn 6045 |
. . . . . 6
⊢ (𝐹:𝐼⟶ℕ0 → 𝐹 Fn 𝐼) |
8 | 6, 7 | syl 17 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → 𝐹 Fn 𝐼) |
9 | | simpr2 1068 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → 𝐺:𝐼⟶ℕ0) |
10 | | ffn 6045 |
. . . . . 6
⊢ (𝐺:𝐼⟶ℕ0 → 𝐺 Fn 𝐼) |
11 | 9, 10 | syl 17 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → 𝐺 Fn 𝐼) |
12 | | simpl 473 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → 𝐼 ∈ 𝑉) |
13 | | inidm 3822 |
. . . . 5
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
14 | 8, 11, 12, 12, 13 | offn 6908 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → (𝐹 ∘𝑓
− 𝐺) Fn 𝐼) |
15 | | eqidd 2623 |
. . . . . . 7
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) = (𝐹‘𝑥)) |
16 | | eqidd 2623 |
. . . . . . 7
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) ∧ 𝑥 ∈ 𝐼) → (𝐺‘𝑥) = (𝐺‘𝑥)) |
17 | 8, 11, 12, 12, 13, 15, 16 | ofval 6906 |
. . . . . 6
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) ∧ 𝑥 ∈ 𝐼) → ((𝐹 ∘𝑓 − 𝐺)‘𝑥) = ((𝐹‘𝑥) − (𝐺‘𝑥))) |
18 | | simpr3 1069 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → 𝐺 ∘𝑟
≤ 𝐹) |
19 | 11, 8, 12, 12, 13, 16, 15 | ofrfval 6905 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → (𝐺 ∘𝑟
≤ 𝐹 ↔ ∀𝑥 ∈ 𝐼 (𝐺‘𝑥) ≤ (𝐹‘𝑥))) |
20 | 18, 19 | mpbid 222 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) →
∀𝑥 ∈ 𝐼 (𝐺‘𝑥) ≤ (𝐹‘𝑥)) |
21 | 20 | r19.21bi 2932 |
. . . . . . 7
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) ∧ 𝑥 ∈ 𝐼) → (𝐺‘𝑥) ≤ (𝐹‘𝑥)) |
22 | 9 | ffvelrnda 6359 |
. . . . . . . 8
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) ∧ 𝑥 ∈ 𝐼) → (𝐺‘𝑥) ∈
ℕ0) |
23 | 6 | ffvelrnda 6359 |
. . . . . . . 8
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) ∈
ℕ0) |
24 | | nn0sub 11343 |
. . . . . . . 8
⊢ (((𝐺‘𝑥) ∈ ℕ0 ∧ (𝐹‘𝑥) ∈ ℕ0) → ((𝐺‘𝑥) ≤ (𝐹‘𝑥) ↔ ((𝐹‘𝑥) − (𝐺‘𝑥)) ∈
ℕ0)) |
25 | 22, 23, 24 | syl2anc 693 |
. . . . . . 7
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) ∧ 𝑥 ∈ 𝐼) → ((𝐺‘𝑥) ≤ (𝐹‘𝑥) ↔ ((𝐹‘𝑥) − (𝐺‘𝑥)) ∈
ℕ0)) |
26 | 21, 25 | mpbid 222 |
. . . . . 6
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) ∧ 𝑥 ∈ 𝐼) → ((𝐹‘𝑥) − (𝐺‘𝑥)) ∈
ℕ0) |
27 | 17, 26 | eqeltrd 2701 |
. . . . 5
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) ∧ 𝑥 ∈ 𝐼) → ((𝐹 ∘𝑓 − 𝐺)‘𝑥) ∈
ℕ0) |
28 | 27 | ralrimiva 2966 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) →
∀𝑥 ∈ 𝐼 ((𝐹 ∘𝑓 − 𝐺)‘𝑥) ∈
ℕ0) |
29 | | ffnfv 6388 |
. . . 4
⊢ ((𝐹 ∘𝑓
− 𝐺):𝐼⟶ℕ0
↔ ((𝐹
∘𝑓 − 𝐺) Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 ((𝐹 ∘𝑓 − 𝐺)‘𝑥) ∈
ℕ0)) |
30 | 14, 28, 29 | sylanbrc 698 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → (𝐹 ∘𝑓
− 𝐺):𝐼⟶ℕ0) |
31 | 5 | simprd 479 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → (◡𝐹 “ ℕ) ∈
Fin) |
32 | 22 | nn0ge0d 11354 |
. . . . . . . 8
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) ∧ 𝑥 ∈ 𝐼) → 0 ≤ (𝐺‘𝑥)) |
33 | | nn0re 11301 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) ∈ ℕ0 → (𝐹‘𝑥) ∈ ℝ) |
34 | | nn0re 11301 |
. . . . . . . . . 10
⊢ ((𝐺‘𝑥) ∈ ℕ0 → (𝐺‘𝑥) ∈ ℝ) |
35 | | subge02 10544 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑥) ∈ ℝ ∧ (𝐺‘𝑥) ∈ ℝ) → (0 ≤ (𝐺‘𝑥) ↔ ((𝐹‘𝑥) − (𝐺‘𝑥)) ≤ (𝐹‘𝑥))) |
36 | 33, 34, 35 | syl2an 494 |
. . . . . . . . 9
⊢ (((𝐹‘𝑥) ∈ ℕ0 ∧ (𝐺‘𝑥) ∈ ℕ0) → (0 ≤
(𝐺‘𝑥) ↔ ((𝐹‘𝑥) − (𝐺‘𝑥)) ≤ (𝐹‘𝑥))) |
37 | 23, 22, 36 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) ∧ 𝑥 ∈ 𝐼) → (0 ≤ (𝐺‘𝑥) ↔ ((𝐹‘𝑥) − (𝐺‘𝑥)) ≤ (𝐹‘𝑥))) |
38 | 32, 37 | mpbid 222 |
. . . . . . 7
⊢ (((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) ∧ 𝑥 ∈ 𝐼) → ((𝐹‘𝑥) − (𝐺‘𝑥)) ≤ (𝐹‘𝑥)) |
39 | 38 | ralrimiva 2966 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) →
∀𝑥 ∈ 𝐼 ((𝐹‘𝑥) − (𝐺‘𝑥)) ≤ (𝐹‘𝑥)) |
40 | 14, 8, 12, 12, 13, 17, 15 | ofrfval 6905 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → ((𝐹 ∘𝑓
− 𝐺)
∘𝑟 ≤ 𝐹 ↔ ∀𝑥 ∈ 𝐼 ((𝐹‘𝑥) − (𝐺‘𝑥)) ≤ (𝐹‘𝑥))) |
41 | 39, 40 | mpbird 247 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → (𝐹 ∘𝑓
− 𝐺)
∘𝑟 ≤ 𝐹) |
42 | 2 | psrbaglesupp 19368 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ (𝐹 ∘𝑓 − 𝐺):𝐼⟶ℕ0 ∧ (𝐹 ∘𝑓
− 𝐺)
∘𝑟 ≤ 𝐹)) → (◡(𝐹 ∘𝑓 − 𝐺) “ ℕ) ⊆
(◡𝐹 “ ℕ)) |
43 | 12, 1, 30, 41, 42 | syl13anc 1328 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → (◡(𝐹 ∘𝑓 − 𝐺) “ ℕ) ⊆
(◡𝐹 “ ℕ)) |
44 | | ssfi 8180 |
. . . 4
⊢ (((◡𝐹 “ ℕ) ∈ Fin ∧ (◡(𝐹 ∘𝑓 − 𝐺) “ ℕ) ⊆
(◡𝐹 “ ℕ)) → (◡(𝐹 ∘𝑓 − 𝐺) “ ℕ) ∈
Fin) |
45 | 31, 43, 44 | syl2anc 693 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → (◡(𝐹 ∘𝑓 − 𝐺) “ ℕ) ∈
Fin) |
46 | 2 | psrbag 19364 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → ((𝐹 ∘𝑓 − 𝐺) ∈ 𝐷 ↔ ((𝐹 ∘𝑓 − 𝐺):𝐼⟶ℕ0 ∧ (◡(𝐹 ∘𝑓 − 𝐺) “ ℕ) ∈
Fin))) |
47 | 46 | adantr 481 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → ((𝐹 ∘𝑓
− 𝐺) ∈ 𝐷 ↔ ((𝐹 ∘𝑓 − 𝐺):𝐼⟶ℕ0 ∧ (◡(𝐹 ∘𝑓 − 𝐺) “ ℕ) ∈
Fin))) |
48 | 30, 45, 47 | mpbir2and 957 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → (𝐹 ∘𝑓
− 𝐺) ∈ 𝐷) |
49 | 48, 41 | jca 554 |
1
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟
≤ 𝐹)) → ((𝐹 ∘𝑓
− 𝐺) ∈ 𝐷 ∧ (𝐹 ∘𝑓 − 𝐺) ∘𝑟
≤ 𝐹)) |