Step | Hyp | Ref
| Expression |
1 | | simprr 792 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)}) |
2 | | breq1 4586 |
. . . . . 6
⊢ (𝑥 = 𝑌 → (𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋) ↔ 𝑌 ∘𝑟
≤ (𝐹
∘𝑓 − 𝑋))) |
3 | 2 | elrab 3331 |
. . . . 5
⊢ (𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)} ↔ (𝑌 ∈ 𝐷 ∧ 𝑌 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋))) |
4 | 1, 3 | sylib 207 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → (𝑌 ∈ 𝐷 ∧ 𝑌 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋))) |
5 | 4 | simpld 474 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑌 ∈ 𝐷) |
6 | 4 | simprd 478 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑌 ∘𝑟
≤ (𝐹
∘𝑓 − 𝑋)) |
7 | | gsumbagdiag.i |
. . . . . . 7
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
8 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝐼 ∈ 𝑉) |
9 | | gsumbagdiag.f |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ 𝐷) |
10 | 9 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝐹 ∈ 𝐷) |
11 | | simprl 790 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑋 ∈ 𝑆) |
12 | | breq1 4586 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑋 → (𝑦 ∘𝑟 ≤ 𝐹 ↔ 𝑋 ∘𝑟 ≤ 𝐹)) |
13 | | psrbagconf1o.1 |
. . . . . . . . . 10
⊢ 𝑆 = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝐹} |
14 | 12, 13 | elrab2 3333 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝑆 ↔ (𝑋 ∈ 𝐷 ∧ 𝑋 ∘𝑟 ≤ 𝐹)) |
15 | 11, 14 | sylib 207 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → (𝑋 ∈ 𝐷 ∧ 𝑋 ∘𝑟 ≤ 𝐹)) |
16 | 15 | simpld 474 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑋 ∈ 𝐷) |
17 | | psrbag.d |
. . . . . . . 8
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin} |
18 | 17 | psrbagf 19186 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐷) → 𝑋:𝐼⟶ℕ0) |
19 | 8, 16, 18 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑋:𝐼⟶ℕ0) |
20 | 15 | simprd 478 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑋 ∘𝑟
≤ 𝐹) |
21 | 17 | psrbagcon 19192 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝑋:𝐼⟶ℕ0 ∧ 𝑋 ∘𝑟
≤ 𝐹)) → ((𝐹 ∘𝑓
− 𝑋) ∈ 𝐷 ∧ (𝐹 ∘𝑓 − 𝑋) ∘𝑟
≤ 𝐹)) |
22 | 8, 10, 19, 20, 21 | syl13anc 1320 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) →
((𝐹
∘𝑓 − 𝑋) ∈ 𝐷 ∧ (𝐹 ∘𝑓 − 𝑋) ∘𝑟
≤ 𝐹)) |
23 | 22 | simprd 478 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → (𝐹 ∘𝑓
− 𝑋)
∘𝑟 ≤ 𝐹) |
24 | 17 | psrbagf 19186 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷) → 𝑌:𝐼⟶ℕ0) |
25 | 8, 5, 24 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑌:𝐼⟶ℕ0) |
26 | 22 | simpld 474 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → (𝐹 ∘𝑓
− 𝑋) ∈ 𝐷) |
27 | 17 | psrbagf 19186 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∘𝑓 − 𝑋) ∈ 𝐷) → (𝐹 ∘𝑓 − 𝑋):𝐼⟶ℕ0) |
28 | 8, 26, 27 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → (𝐹 ∘𝑓
− 𝑋):𝐼⟶ℕ0) |
29 | 17 | psrbagf 19186 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) → 𝐹:𝐼⟶ℕ0) |
30 | 8, 10, 29 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝐹:𝐼⟶ℕ0) |
31 | | nn0re 11178 |
. . . . . . 7
⊢ (𝑢 ∈ ℕ0
→ 𝑢 ∈
ℝ) |
32 | | nn0re 11178 |
. . . . . . 7
⊢ (𝑣 ∈ ℕ0
→ 𝑣 ∈
ℝ) |
33 | | nn0re 11178 |
. . . . . . 7
⊢ (𝑤 ∈ ℕ0
→ 𝑤 ∈
ℝ) |
34 | | letr 10010 |
. . . . . . 7
⊢ ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ ∧ 𝑤 ∈ ℝ) → ((𝑢 ≤ 𝑣 ∧ 𝑣 ≤ 𝑤) → 𝑢 ≤ 𝑤)) |
35 | 31, 32, 33, 34 | syl3an 1360 |
. . . . . 6
⊢ ((𝑢 ∈ ℕ0
∧ 𝑣 ∈
ℕ0 ∧ 𝑤
∈ ℕ0) → ((𝑢 ≤ 𝑣 ∧ 𝑣 ≤ 𝑤) → 𝑢 ≤ 𝑤)) |
36 | 35 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) ∧ (𝑢 ∈ ℕ0
∧ 𝑣 ∈
ℕ0 ∧ 𝑤
∈ ℕ0)) → ((𝑢 ≤ 𝑣 ∧ 𝑣 ≤ 𝑤) → 𝑢 ≤ 𝑤)) |
37 | 8, 25, 28, 30, 36 | caoftrn 6830 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) →
((𝑌
∘𝑟 ≤ (𝐹 ∘𝑓 − 𝑋) ∧ (𝐹 ∘𝑓 − 𝑋) ∘𝑟
≤ 𝐹) → 𝑌 ∘𝑟
≤ 𝐹)) |
38 | 6, 23, 37 | mp2and 711 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑌 ∘𝑟
≤ 𝐹) |
39 | | breq1 4586 |
. . . 4
⊢ (𝑦 = 𝑌 → (𝑦 ∘𝑟 ≤ 𝐹 ↔ 𝑌 ∘𝑟 ≤ 𝐹)) |
40 | 39, 13 | elrab2 3333 |
. . 3
⊢ (𝑌 ∈ 𝑆 ↔ (𝑌 ∈ 𝐷 ∧ 𝑌 ∘𝑟 ≤ 𝐹)) |
41 | 5, 38, 40 | sylanbrc 695 |
. 2
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑌 ∈ 𝑆) |
42 | 19 | ffvelrnda 6267 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) ∧ 𝑧 ∈ 𝐼) → (𝑋‘𝑧) ∈
ℕ0) |
43 | 25 | ffvelrnda 6267 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) ∧ 𝑧 ∈ 𝐼) → (𝑌‘𝑧) ∈
ℕ0) |
44 | 30 | ffvelrnda 6267 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) ∈
ℕ0) |
45 | | nn0re 11178 |
. . . . . . . 8
⊢ ((𝑋‘𝑧) ∈ ℕ0 → (𝑋‘𝑧) ∈ ℝ) |
46 | | nn0re 11178 |
. . . . . . . 8
⊢ ((𝑌‘𝑧) ∈ ℕ0 → (𝑌‘𝑧) ∈ ℝ) |
47 | | nn0re 11178 |
. . . . . . . 8
⊢ ((𝐹‘𝑧) ∈ ℕ0 → (𝐹‘𝑧) ∈ ℝ) |
48 | | leaddsub2 10384 |
. . . . . . . . 9
⊢ (((𝑋‘𝑧) ∈ ℝ ∧ (𝑌‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) ∈ ℝ) → (((𝑋‘𝑧) + (𝑌‘𝑧)) ≤ (𝐹‘𝑧) ↔ (𝑌‘𝑧) ≤ ((𝐹‘𝑧) − (𝑋‘𝑧)))) |
49 | | leaddsub 10383 |
. . . . . . . . 9
⊢ (((𝑋‘𝑧) ∈ ℝ ∧ (𝑌‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) ∈ ℝ) → (((𝑋‘𝑧) + (𝑌‘𝑧)) ≤ (𝐹‘𝑧) ↔ (𝑋‘𝑧) ≤ ((𝐹‘𝑧) − (𝑌‘𝑧)))) |
50 | 48, 49 | bitr3d 269 |
. . . . . . . 8
⊢ (((𝑋‘𝑧) ∈ ℝ ∧ (𝑌‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) ∈ ℝ) → ((𝑌‘𝑧) ≤ ((𝐹‘𝑧) − (𝑋‘𝑧)) ↔ (𝑋‘𝑧) ≤ ((𝐹‘𝑧) − (𝑌‘𝑧)))) |
51 | 45, 46, 47, 50 | syl3an 1360 |
. . . . . . 7
⊢ (((𝑋‘𝑧) ∈ ℕ0 ∧ (𝑌‘𝑧) ∈ ℕ0 ∧ (𝐹‘𝑧) ∈ ℕ0) → ((𝑌‘𝑧) ≤ ((𝐹‘𝑧) − (𝑋‘𝑧)) ↔ (𝑋‘𝑧) ≤ ((𝐹‘𝑧) − (𝑌‘𝑧)))) |
52 | 42, 43, 44, 51 | syl3anc 1318 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) ∧ 𝑧 ∈ 𝐼) → ((𝑌‘𝑧) ≤ ((𝐹‘𝑧) − (𝑋‘𝑧)) ↔ (𝑋‘𝑧) ≤ ((𝐹‘𝑧) − (𝑌‘𝑧)))) |
53 | 52 | ralbidva 2968 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) →
(∀𝑧 ∈ 𝐼 (𝑌‘𝑧) ≤ ((𝐹‘𝑧) − (𝑋‘𝑧)) ↔ ∀𝑧 ∈ 𝐼 (𝑋‘𝑧) ≤ ((𝐹‘𝑧) − (𝑌‘𝑧)))) |
54 | | ovex 6577 |
. . . . . . 7
⊢ ((𝐹‘𝑧) − (𝑋‘𝑧)) ∈ V |
55 | 54 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) ∧ 𝑧 ∈ 𝐼) → ((𝐹‘𝑧) − (𝑋‘𝑧)) ∈ V) |
56 | 25 | feqmptd 6159 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑌 = (𝑧 ∈ 𝐼 ↦ (𝑌‘𝑧))) |
57 | | ffn 5958 |
. . . . . . . 8
⊢ (𝐹:𝐼⟶ℕ0 → 𝐹 Fn 𝐼) |
58 | 30, 57 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝐹 Fn 𝐼) |
59 | | ffn 5958 |
. . . . . . . 8
⊢ (𝑋:𝐼⟶ℕ0 → 𝑋 Fn 𝐼) |
60 | 19, 59 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑋 Fn 𝐼) |
61 | | inidm 3784 |
. . . . . . 7
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
62 | | eqidd 2611 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) = (𝐹‘𝑧)) |
63 | | eqidd 2611 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) ∧ 𝑧 ∈ 𝐼) → (𝑋‘𝑧) = (𝑋‘𝑧)) |
64 | 58, 60, 8, 8, 61, 62, 63 | offval 6802 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → (𝐹 ∘𝑓
− 𝑋) = (𝑧 ∈ 𝐼 ↦ ((𝐹‘𝑧) − (𝑋‘𝑧)))) |
65 | 8, 43, 55, 56, 64 | ofrfval2 6813 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → (𝑌 ∘𝑟
≤ (𝐹
∘𝑓 − 𝑋) ↔ ∀𝑧 ∈ 𝐼 (𝑌‘𝑧) ≤ ((𝐹‘𝑧) − (𝑋‘𝑧)))) |
66 | | ovex 6577 |
. . . . . . 7
⊢ ((𝐹‘𝑧) − (𝑌‘𝑧)) ∈ V |
67 | 66 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) ∧ 𝑧 ∈ 𝐼) → ((𝐹‘𝑧) − (𝑌‘𝑧)) ∈ V) |
68 | 19 | feqmptd 6159 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑋 = (𝑧 ∈ 𝐼 ↦ (𝑋‘𝑧))) |
69 | | ffn 5958 |
. . . . . . . 8
⊢ (𝑌:𝐼⟶ℕ0 → 𝑌 Fn 𝐼) |
70 | 25, 69 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑌 Fn 𝐼) |
71 | | eqidd 2611 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) ∧ 𝑧 ∈ 𝐼) → (𝑌‘𝑧) = (𝑌‘𝑧)) |
72 | 58, 70, 8, 8, 61, 62, 71 | offval 6802 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → (𝐹 ∘𝑓
− 𝑌) = (𝑧 ∈ 𝐼 ↦ ((𝐹‘𝑧) − (𝑌‘𝑧)))) |
73 | 8, 42, 67, 68, 72 | ofrfval2 6813 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → (𝑋 ∘𝑟
≤ (𝐹
∘𝑓 − 𝑌) ↔ ∀𝑧 ∈ 𝐼 (𝑋‘𝑧) ≤ ((𝐹‘𝑧) − (𝑌‘𝑧)))) |
74 | 53, 65, 73 | 3bitr4d 299 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → (𝑌 ∘𝑟
≤ (𝐹
∘𝑓 − 𝑋) ↔ 𝑋 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑌))) |
75 | 6, 74 | mpbid 221 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑋 ∘𝑟
≤ (𝐹
∘𝑓 − 𝑌)) |
76 | | breq1 4586 |
. . . 4
⊢ (𝑥 = 𝑋 → (𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑌) ↔ 𝑋 ∘𝑟
≤ (𝐹
∘𝑓 − 𝑌))) |
77 | 76 | elrab 3331 |
. . 3
⊢ (𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑌)} ↔ (𝑋 ∈ 𝐷 ∧ 𝑋 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑌))) |
78 | 16, 75, 77 | sylanbrc 695 |
. 2
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑌)}) |
79 | 41, 78 | jca 553 |
1
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑋)})) → (𝑌 ∈ 𝑆 ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑌)})) |