Step | Hyp | Ref
| Expression |
1 | | simprr 813 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)}) |
2 | | breq1 4807 |
. . . . . 6
⊢ (𝑥 = 𝑌 → (𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋) ↔ 𝑌 ∘𝑟
≤ (𝐹
∘𝑓 − 𝑋))) |
3 | 2 | elrab 3504 |
. . . . 5
⊢ (𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)} ↔ (𝑌 ∈ 𝐷 ∧ 𝑌 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋))) |
4 | 1, 3 | sylib 208 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → (𝑌 ∈ 𝐷 ∧ 𝑌 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋))) |
5 | 4 | simpld 477 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑌 ∈ 𝐷) |
6 | 4 | simprd 482 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑌 ∘𝑟
≤ (𝐹
∘𝑓 − 𝑋)) |
7 | | gsumbagdiag.i |
. . . . . . 7
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
8 | 7 | adantr 472 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝐼 ∈ 𝑉) |
9 | | gsumbagdiag.f |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ 𝐷) |
10 | 9 | adantr 472 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝐹 ∈ 𝐷) |
11 | | simprl 811 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑋 ∈ 𝑆) |
12 | | breq1 4807 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑋 → (𝑦 ∘𝑟 ≤ 𝐹 ↔ 𝑋 ∘𝑟 ≤ 𝐹)) |
13 | | psrbagconf1o.1 |
. . . . . . . . . 10
⊢ 𝑆 = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝐹} |
14 | 12, 13 | elrab2 3507 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝑆 ↔ (𝑋 ∈ 𝐷 ∧ 𝑋 ∘𝑟 ≤ 𝐹)) |
15 | 11, 14 | sylib 208 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → (𝑋 ∈ 𝐷 ∧ 𝑋 ∘𝑟 ≤ 𝐹)) |
16 | 15 | simpld 477 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑋 ∈ 𝐷) |
17 | | psrbag.d |
. . . . . . . 8
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin} |
18 | 17 | psrbagf 19567 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐷) → 𝑋:𝐼⟶ℕ0) |
19 | 8, 16, 18 | syl2anc 696 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑋:𝐼⟶ℕ0) |
20 | 15 | simprd 482 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑋 ∘𝑟
≤ 𝐹) |
21 | 17 | psrbagcon 19573 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝑋:𝐼⟶ℕ0 ∧ 𝑋 ∘𝑟
≤ 𝐹)) → ((𝐹 ∘𝑓
− 𝑋) ∈ 𝐷 ∧ (𝐹 ∘𝑓 − 𝑋) ∘𝑟
≤ 𝐹)) |
22 | 8, 10, 19, 20, 21 | syl13anc 1479 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) →
((𝐹
∘𝑓 − 𝑋) ∈ 𝐷 ∧ (𝐹 ∘𝑓 − 𝑋) ∘𝑟
≤ 𝐹)) |
23 | 22 | simprd 482 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → (𝐹 ∘𝑓
− 𝑋)
∘𝑟 ≤ 𝐹) |
24 | 17 | psrbagf 19567 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷) → 𝑌:𝐼⟶ℕ0) |
25 | 8, 5, 24 | syl2anc 696 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑌:𝐼⟶ℕ0) |
26 | 22 | simpld 477 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → (𝐹 ∘𝑓
− 𝑋) ∈ 𝐷) |
27 | 17 | psrbagf 19567 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∘𝑓 − 𝑋) ∈ 𝐷) → (𝐹 ∘𝑓 − 𝑋):𝐼⟶ℕ0) |
28 | 8, 26, 27 | syl2anc 696 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → (𝐹 ∘𝑓
− 𝑋):𝐼⟶ℕ0) |
29 | 17 | psrbagf 19567 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) → 𝐹:𝐼⟶ℕ0) |
30 | 8, 10, 29 | syl2anc 696 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝐹:𝐼⟶ℕ0) |
31 | | nn0re 11493 |
. . . . . . 7
⊢ (𝑢 ∈ ℕ0
→ 𝑢 ∈
ℝ) |
32 | | nn0re 11493 |
. . . . . . 7
⊢ (𝑣 ∈ ℕ0
→ 𝑣 ∈
ℝ) |
33 | | nn0re 11493 |
. . . . . . 7
⊢ (𝑤 ∈ ℕ0
→ 𝑤 ∈
ℝ) |
34 | | letr 10323 |
. . . . . . 7
⊢ ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ ∧ 𝑤 ∈ ℝ) → ((𝑢 ≤ 𝑣 ∧ 𝑣 ≤ 𝑤) → 𝑢 ≤ 𝑤)) |
35 | 31, 32, 33, 34 | syl3an 1164 |
. . . . . 6
⊢ ((𝑢 ∈ ℕ0
∧ 𝑣 ∈
ℕ0 ∧ 𝑤
∈ ℕ0) → ((𝑢 ≤ 𝑣 ∧ 𝑣 ≤ 𝑤) → 𝑢 ≤ 𝑤)) |
36 | 35 | adantl 473 |
. . . . 5
⊢ (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) ∧ (𝑢 ∈ ℕ0
∧ 𝑣 ∈
ℕ0 ∧ 𝑤
∈ ℕ0)) → ((𝑢 ≤ 𝑣 ∧ 𝑣 ≤ 𝑤) → 𝑢 ≤ 𝑤)) |
37 | 8, 25, 28, 30, 36 | caoftrn 7097 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) →
((𝑌
∘𝑟 ≤ (𝐹 ∘𝑓 − 𝑋) ∧ (𝐹 ∘𝑓 − 𝑋) ∘𝑟
≤ 𝐹) → 𝑌 ∘𝑟
≤ 𝐹)) |
38 | 6, 23, 37 | mp2and 717 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑌 ∘𝑟
≤ 𝐹) |
39 | | breq1 4807 |
. . . 4
⊢ (𝑦 = 𝑌 → (𝑦 ∘𝑟 ≤ 𝐹 ↔ 𝑌 ∘𝑟 ≤ 𝐹)) |
40 | 39, 13 | elrab2 3507 |
. . 3
⊢ (𝑌 ∈ 𝑆 ↔ (𝑌 ∈ 𝐷 ∧ 𝑌 ∘𝑟 ≤ 𝐹)) |
41 | 5, 38, 40 | sylanbrc 701 |
. 2
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑌 ∈ 𝑆) |
42 | 19 | ffvelrnda 6522 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) ∧ 𝑧 ∈ 𝐼) → (𝑋‘𝑧) ∈
ℕ0) |
43 | 25 | ffvelrnda 6522 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) ∧ 𝑧 ∈ 𝐼) → (𝑌‘𝑧) ∈
ℕ0) |
44 | 30 | ffvelrnda 6522 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) ∈
ℕ0) |
45 | | nn0re 11493 |
. . . . . . . 8
⊢ ((𝑋‘𝑧) ∈ ℕ0 → (𝑋‘𝑧) ∈ ℝ) |
46 | | nn0re 11493 |
. . . . . . . 8
⊢ ((𝑌‘𝑧) ∈ ℕ0 → (𝑌‘𝑧) ∈ ℝ) |
47 | | nn0re 11493 |
. . . . . . . 8
⊢ ((𝐹‘𝑧) ∈ ℕ0 → (𝐹‘𝑧) ∈ ℝ) |
48 | | leaddsub2 10697 |
. . . . . . . . 9
⊢ (((𝑋‘𝑧) ∈ ℝ ∧ (𝑌‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) ∈ ℝ) → (((𝑋‘𝑧) + (𝑌‘𝑧)) ≤ (𝐹‘𝑧) ↔ (𝑌‘𝑧) ≤ ((𝐹‘𝑧) − (𝑋‘𝑧)))) |
49 | | leaddsub 10696 |
. . . . . . . . 9
⊢ (((𝑋‘𝑧) ∈ ℝ ∧ (𝑌‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) ∈ ℝ) → (((𝑋‘𝑧) + (𝑌‘𝑧)) ≤ (𝐹‘𝑧) ↔ (𝑋‘𝑧) ≤ ((𝐹‘𝑧) − (𝑌‘𝑧)))) |
50 | 48, 49 | bitr3d 270 |
. . . . . . . 8
⊢ (((𝑋‘𝑧) ∈ ℝ ∧ (𝑌‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) ∈ ℝ) → ((𝑌‘𝑧) ≤ ((𝐹‘𝑧) − (𝑋‘𝑧)) ↔ (𝑋‘𝑧) ≤ ((𝐹‘𝑧) − (𝑌‘𝑧)))) |
51 | 45, 46, 47, 50 | syl3an 1164 |
. . . . . . 7
⊢ (((𝑋‘𝑧) ∈ ℕ0 ∧ (𝑌‘𝑧) ∈ ℕ0 ∧ (𝐹‘𝑧) ∈ ℕ0) → ((𝑌‘𝑧) ≤ ((𝐹‘𝑧) − (𝑋‘𝑧)) ↔ (𝑋‘𝑧) ≤ ((𝐹‘𝑧) − (𝑌‘𝑧)))) |
52 | 42, 43, 44, 51 | syl3anc 1477 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) ∧ 𝑧 ∈ 𝐼) → ((𝑌‘𝑧) ≤ ((𝐹‘𝑧) − (𝑋‘𝑧)) ↔ (𝑋‘𝑧) ≤ ((𝐹‘𝑧) − (𝑌‘𝑧)))) |
53 | 52 | ralbidva 3123 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) →
(∀𝑧 ∈ 𝐼 (𝑌‘𝑧) ≤ ((𝐹‘𝑧) − (𝑋‘𝑧)) ↔ ∀𝑧 ∈ 𝐼 (𝑋‘𝑧) ≤ ((𝐹‘𝑧) − (𝑌‘𝑧)))) |
54 | | ovexd 6843 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) ∧ 𝑧 ∈ 𝐼) → ((𝐹‘𝑧) − (𝑋‘𝑧)) ∈ V) |
55 | 25 | feqmptd 6411 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑌 = (𝑧 ∈ 𝐼 ↦ (𝑌‘𝑧))) |
56 | | ffn 6206 |
. . . . . . . 8
⊢ (𝐹:𝐼⟶ℕ0 → 𝐹 Fn 𝐼) |
57 | 30, 56 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝐹 Fn 𝐼) |
58 | | ffn 6206 |
. . . . . . . 8
⊢ (𝑋:𝐼⟶ℕ0 → 𝑋 Fn 𝐼) |
59 | 19, 58 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑋 Fn 𝐼) |
60 | | inidm 3965 |
. . . . . . 7
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
61 | | eqidd 2761 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) = (𝐹‘𝑧)) |
62 | | eqidd 2761 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) ∧ 𝑧 ∈ 𝐼) → (𝑋‘𝑧) = (𝑋‘𝑧)) |
63 | 57, 59, 8, 8, 60, 61, 62 | offval 7069 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → (𝐹 ∘𝑓
− 𝑋) = (𝑧 ∈ 𝐼 ↦ ((𝐹‘𝑧) − (𝑋‘𝑧)))) |
64 | 8, 43, 54, 55, 63 | ofrfval2 7080 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → (𝑌 ∘𝑟
≤ (𝐹
∘𝑓 − 𝑋) ↔ ∀𝑧 ∈ 𝐼 (𝑌‘𝑧) ≤ ((𝐹‘𝑧) − (𝑋‘𝑧)))) |
65 | | ovexd 6843 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) ∧ 𝑧 ∈ 𝐼) → ((𝐹‘𝑧) − (𝑌‘𝑧)) ∈ V) |
66 | 19 | feqmptd 6411 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑋 = (𝑧 ∈ 𝐼 ↦ (𝑋‘𝑧))) |
67 | | ffn 6206 |
. . . . . . . 8
⊢ (𝑌:𝐼⟶ℕ0 → 𝑌 Fn 𝐼) |
68 | 25, 67 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑌 Fn 𝐼) |
69 | | eqidd 2761 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) ∧ 𝑧 ∈ 𝐼) → (𝑌‘𝑧) = (𝑌‘𝑧)) |
70 | 57, 68, 8, 8, 60, 61, 69 | offval 7069 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → (𝐹 ∘𝑓
− 𝑌) = (𝑧 ∈ 𝐼 ↦ ((𝐹‘𝑧) − (𝑌‘𝑧)))) |
71 | 8, 42, 65, 66, 70 | ofrfval2 7080 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → (𝑋 ∘𝑟
≤ (𝐹
∘𝑓 − 𝑌) ↔ ∀𝑧 ∈ 𝐼 (𝑋‘𝑧) ≤ ((𝐹‘𝑧) − (𝑌‘𝑧)))) |
72 | 53, 64, 71 | 3bitr4d 300 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → (𝑌 ∘𝑟
≤ (𝐹
∘𝑓 − 𝑋) ↔ 𝑋 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑌))) |
73 | 6, 72 | mpbid 222 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑋 ∘𝑟
≤ (𝐹
∘𝑓 − 𝑌)) |
74 | | breq1 4807 |
. . . 4
⊢ (𝑥 = 𝑋 → (𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑌) ↔ 𝑋 ∘𝑟
≤ (𝐹
∘𝑓 − 𝑌))) |
75 | 74 | elrab 3504 |
. . 3
⊢ (𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑌)} ↔ (𝑋 ∈ 𝐷 ∧ 𝑋 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑌))) |
76 | 16, 73, 75 | sylanbrc 701 |
. 2
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑌)}) |
77 | 41, 76 | jca 555 |
1
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → (𝑌 ∈ 𝑆 ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑌)})) |