| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elrabi 3687 | . . . . 5
⊢ (𝑋 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹} → 𝑋 ∈ 𝐷) | 
| 2 |  | psrbagconf1o.s | . . . . 5
⊢ 𝑆 = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹} | 
| 3 | 1, 2 | eleq2s 2859 | . . . 4
⊢ (𝑋 ∈ 𝑆 → 𝑋 ∈ 𝐷) | 
| 4 | 3 | 3ad2ant3 1136 | . . 3
⊢ ((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) → 𝑋 ∈ 𝐷) | 
| 5 |  | simp2 1138 | . . 3
⊢ ((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) → 𝐺 ∈ 𝐷) | 
| 6 |  | psrbag.d | . . . 4
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin} | 
| 7 | 6 | psrbagaddcl 21944 | . . 3
⊢ ((𝑋 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷) → (𝑋 ∘f + 𝐺) ∈ 𝐷) | 
| 8 | 4, 5, 7 | syl2anc 584 | . 2
⊢ ((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) → (𝑋 ∘f + 𝐺) ∈ 𝐷) | 
| 9 | 6 | psrbagf 21938 | . . . . . . . 8
⊢ (𝑋 ∈ 𝐷 → 𝑋:𝐼⟶ℕ0) | 
| 10 | 4, 9 | syl 17 | . . . . . . 7
⊢ ((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) → 𝑋:𝐼⟶ℕ0) | 
| 11 | 10 | ffvelcdmda 7104 | . . . . . 6
⊢ (((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) ∧ 𝑥 ∈ 𝐼) → (𝑋‘𝑥) ∈
ℕ0) | 
| 12 | 11 | nn0red 12588 | . . . . 5
⊢ (((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) ∧ 𝑥 ∈ 𝐼) → (𝑋‘𝑥) ∈ ℝ) | 
| 13 | 6 | psrbagf 21938 | . . . . . . . 8
⊢ (𝐹 ∈ 𝐷 → 𝐹:𝐼⟶ℕ0) | 
| 14 | 13 | 3ad2ant1 1134 | . . . . . . 7
⊢ ((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) → 𝐹:𝐼⟶ℕ0) | 
| 15 | 14 | ffvelcdmda 7104 | . . . . . 6
⊢ (((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) ∈
ℕ0) | 
| 16 | 15 | nn0red 12588 | . . . . 5
⊢ (((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) ∈ ℝ) | 
| 17 | 6 | psrbagf 21938 | . . . . . . . 8
⊢ (𝐺 ∈ 𝐷 → 𝐺:𝐼⟶ℕ0) | 
| 18 | 17 | 3ad2ant2 1135 | . . . . . . 7
⊢ ((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) → 𝐺:𝐼⟶ℕ0) | 
| 19 | 18 | ffvelcdmda 7104 | . . . . . 6
⊢ (((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) ∧ 𝑥 ∈ 𝐼) → (𝐺‘𝑥) ∈
ℕ0) | 
| 20 | 19 | nn0red 12588 | . . . . 5
⊢ (((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) ∧ 𝑥 ∈ 𝐼) → (𝐺‘𝑥) ∈ ℝ) | 
| 21 |  | breq1 5146 | . . . . . . . . . 10
⊢ (𝑦 = 𝑋 → (𝑦 ∘r ≤ 𝐹 ↔ 𝑋 ∘r ≤ 𝐹)) | 
| 22 | 21, 2 | elrab2 3695 | . . . . . . . . 9
⊢ (𝑋 ∈ 𝑆 ↔ (𝑋 ∈ 𝐷 ∧ 𝑋 ∘r ≤ 𝐹)) | 
| 23 | 22 | simprbi 496 | . . . . . . . 8
⊢ (𝑋 ∈ 𝑆 → 𝑋 ∘r ≤ 𝐹) | 
| 24 | 23 | 3ad2ant3 1136 | . . . . . . 7
⊢ ((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) → 𝑋 ∘r ≤ 𝐹) | 
| 25 | 9 | ffnd 6737 | . . . . . . . . . 10
⊢ (𝑋 ∈ 𝐷 → 𝑋 Fn 𝐼) | 
| 26 | 3, 25 | syl 17 | . . . . . . . . 9
⊢ (𝑋 ∈ 𝑆 → 𝑋 Fn 𝐼) | 
| 27 | 26 | 3ad2ant3 1136 | . . . . . . . 8
⊢ ((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) → 𝑋 Fn 𝐼) | 
| 28 | 13 | ffnd 6737 | . . . . . . . . 9
⊢ (𝐹 ∈ 𝐷 → 𝐹 Fn 𝐼) | 
| 29 | 28 | 3ad2ant1 1134 | . . . . . . . 8
⊢ ((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) → 𝐹 Fn 𝐼) | 
| 30 |  | id 22 | . . . . . . . . . 10
⊢ (𝐹 ∈ 𝐷 → 𝐹 ∈ 𝐷) | 
| 31 | 30, 28 | fndmexd 7926 | . . . . . . . . 9
⊢ (𝐹 ∈ 𝐷 → 𝐼 ∈ V) | 
| 32 | 31 | 3ad2ant1 1134 | . . . . . . . 8
⊢ ((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) → 𝐼 ∈ V) | 
| 33 |  | inidm 4227 | . . . . . . . 8
⊢ (𝐼 ∩ 𝐼) = 𝐼 | 
| 34 |  | eqidd 2738 | . . . . . . . 8
⊢ (((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) ∧ 𝑥 ∈ 𝐼) → (𝑋‘𝑥) = (𝑋‘𝑥)) | 
| 35 |  | eqidd 2738 | . . . . . . . 8
⊢ (((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) = (𝐹‘𝑥)) | 
| 36 | 27, 29, 32, 32, 33, 34, 35 | ofrfval 7707 | . . . . . . 7
⊢ ((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) → (𝑋 ∘r ≤ 𝐹 ↔ ∀𝑥 ∈ 𝐼 (𝑋‘𝑥) ≤ (𝐹‘𝑥))) | 
| 37 | 24, 36 | mpbid 232 | . . . . . 6
⊢ ((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) → ∀𝑥 ∈ 𝐼 (𝑋‘𝑥) ≤ (𝐹‘𝑥)) | 
| 38 | 37 | r19.21bi 3251 | . . . . 5
⊢ (((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) ∧ 𝑥 ∈ 𝐼) → (𝑋‘𝑥) ≤ (𝐹‘𝑥)) | 
| 39 | 12, 16, 20, 38 | leadd1dd 11877 | . . . 4
⊢ (((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) ∧ 𝑥 ∈ 𝐼) → ((𝑋‘𝑥) + (𝐺‘𝑥)) ≤ ((𝐹‘𝑥) + (𝐺‘𝑥))) | 
| 40 | 39 | ralrimiva 3146 | . . 3
⊢ ((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) → ∀𝑥 ∈ 𝐼 ((𝑋‘𝑥) + (𝐺‘𝑥)) ≤ ((𝐹‘𝑥) + (𝐺‘𝑥))) | 
| 41 | 6 | psrbagf 21938 | . . . . . 6
⊢ ((𝑋 ∘f + 𝐺) ∈ 𝐷 → (𝑋 ∘f + 𝐺):𝐼⟶ℕ0) | 
| 42 | 41 | ffnd 6737 | . . . . 5
⊢ ((𝑋 ∘f + 𝐺) ∈ 𝐷 → (𝑋 ∘f + 𝐺) Fn 𝐼) | 
| 43 | 8, 42 | syl 17 | . . . 4
⊢ ((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) → (𝑋 ∘f + 𝐺) Fn 𝐼) | 
| 44 | 6 | psrbagaddcl 21944 | . . . . . 6
⊢ ((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷) → (𝐹 ∘f + 𝐺) ∈ 𝐷) | 
| 45 | 44 | 3adant3 1133 | . . . . 5
⊢ ((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) → (𝐹 ∘f + 𝐺) ∈ 𝐷) | 
| 46 | 6 | psrbagf 21938 | . . . . . 6
⊢ ((𝐹 ∘f + 𝐺) ∈ 𝐷 → (𝐹 ∘f + 𝐺):𝐼⟶ℕ0) | 
| 47 | 46 | ffnd 6737 | . . . . 5
⊢ ((𝐹 ∘f + 𝐺) ∈ 𝐷 → (𝐹 ∘f + 𝐺) Fn 𝐼) | 
| 48 | 45, 47 | syl 17 | . . . 4
⊢ ((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) → (𝐹 ∘f + 𝐺) Fn 𝐼) | 
| 49 | 17 | ffnd 6737 | . . . . . 6
⊢ (𝐺 ∈ 𝐷 → 𝐺 Fn 𝐼) | 
| 50 | 49 | 3ad2ant2 1135 | . . . . 5
⊢ ((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) → 𝐺 Fn 𝐼) | 
| 51 |  | eqidd 2738 | . . . . 5
⊢ (((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) ∧ 𝑥 ∈ 𝐼) → (𝐺‘𝑥) = (𝐺‘𝑥)) | 
| 52 | 27, 50, 32, 32, 33, 34, 51 | ofval 7708 | . . . 4
⊢ (((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) ∧ 𝑥 ∈ 𝐼) → ((𝑋 ∘f + 𝐺)‘𝑥) = ((𝑋‘𝑥) + (𝐺‘𝑥))) | 
| 53 | 29, 50, 32, 32, 33, 35, 51 | ofval 7708 | . . . 4
⊢ (((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) ∧ 𝑥 ∈ 𝐼) → ((𝐹 ∘f + 𝐺)‘𝑥) = ((𝐹‘𝑥) + (𝐺‘𝑥))) | 
| 54 | 43, 48, 32, 32, 33, 52, 53 | ofrfval 7707 | . . 3
⊢ ((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) → ((𝑋 ∘f + 𝐺) ∘r ≤ (𝐹 ∘f + 𝐺) ↔ ∀𝑥 ∈ 𝐼 ((𝑋‘𝑥) + (𝐺‘𝑥)) ≤ ((𝐹‘𝑥) + (𝐺‘𝑥)))) | 
| 55 | 40, 54 | mpbird 257 | . 2
⊢ ((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) → (𝑋 ∘f + 𝐺) ∘r ≤ (𝐹 ∘f + 𝐺)) | 
| 56 |  | breq1 5146 | . . 3
⊢ (𝑧 = (𝑋 ∘f + 𝐺) → (𝑧 ∘r ≤ (𝐹 ∘f + 𝐺) ↔ (𝑋 ∘f + 𝐺) ∘r ≤ (𝐹 ∘f + 𝐺))) | 
| 57 |  | psrbagleadd1.t | . . 3
⊢ 𝑇 = {𝑧 ∈ 𝐷 ∣ 𝑧 ∘r ≤ (𝐹 ∘f + 𝐺)} | 
| 58 | 56, 57 | elrab2 3695 | . 2
⊢ ((𝑋 ∘f + 𝐺) ∈ 𝑇 ↔ ((𝑋 ∘f + 𝐺) ∈ 𝐷 ∧ (𝑋 ∘f + 𝐺) ∘r ≤ (𝐹 ∘f + 𝐺))) | 
| 59 | 8, 55, 58 | sylanbrc 583 | 1
⊢ ((𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆) → (𝑋 ∘f + 𝐺) ∈ 𝑇) |