Step | Hyp | Ref
| Expression |
1 | | elun 4125 |
. . . 4
⊢ (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 ∈ {𝑧})) |
2 | | velsn 4583 |
. . . . 5
⊢ (𝑤 ∈ {𝑧} ↔ 𝑤 = 𝑧) |
3 | 2 | orbi2i 909 |
. . . 4
⊢ ((𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 ∈ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 = 𝑧)) |
4 | 1, 3 | bitri 277 |
. . 3
⊢ (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 = 𝑧)) |
5 | | elinel2 4173 |
. . . . . . . 8
⊢ (𝑤 ∈ (𝑆 ∩ dom 𝐹) → 𝑤 ∈ dom 𝐹) |
6 | | frrlem11.1 |
. . . . . . . . . 10
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} |
7 | 6 | frrlem1 33123 |
. . . . . . . . 9
⊢ 𝐵 = {𝑝 ∣ ∃𝑞(𝑝 Fn 𝑞 ∧ (𝑞 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑞 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑞) ∧ ∀𝑤 ∈ 𝑞 (𝑝‘𝑤) = (𝑤𝐺(𝑝 ↾ Pred(𝑅, 𝐴, 𝑤))))} |
8 | | frrlem11.2 |
. . . . . . . . 9
⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) |
9 | | breq1 5069 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑞 → (𝑥𝑔𝑢 ↔ 𝑞𝑔𝑢)) |
10 | | breq1 5069 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑞 → (𝑥ℎ𝑣 ↔ 𝑞ℎ𝑣)) |
11 | 9, 10 | anbi12d 632 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑞 → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) ↔ (𝑞𝑔𝑢 ∧ 𝑞ℎ𝑣))) |
12 | 11 | imbi1d 344 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑞 → (((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣) ↔ ((𝑞𝑔𝑢 ∧ 𝑞ℎ𝑣) → 𝑢 = 𝑣))) |
13 | 12 | imbi2d 343 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑞 → (((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) ↔ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑞𝑔𝑢 ∧ 𝑞ℎ𝑣) → 𝑢 = 𝑣)))) |
14 | | frrlem11.3 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) |
15 | 13, 14 | chvarvv 2005 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑞𝑔𝑢 ∧ 𝑞ℎ𝑣) → 𝑢 = 𝑣)) |
16 | 7, 8, 15 | frrlem10 33132 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝐹) → (𝐹‘𝑤) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤)))) |
17 | 5, 16 | sylan2 594 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹‘𝑤) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤)))) |
18 | 17 | adantlr 713 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹‘𝑤) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤)))) |
19 | | frrlem11.4 |
. . . . . . . . 9
⊢ 𝐶 = ((𝐹 ↾ 𝑆) ∪ {〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}) |
20 | 19 | fveq1i 6671 |
. . . . . . . 8
⊢ (𝐶‘𝑤) = (((𝐹 ↾ 𝑆) ∪ {〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉})‘𝑤) |
21 | 6, 8, 14 | frrlem9 33131 |
. . . . . . . . . . . . 13
⊢ (𝜑 → Fun 𝐹) |
22 | | funres 6397 |
. . . . . . . . . . . . 13
⊢ (Fun
𝐹 → Fun (𝐹 ↾ 𝑆)) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → Fun (𝐹 ↾ 𝑆)) |
24 | | dmres 5875 |
. . . . . . . . . . . 12
⊢ dom
(𝐹 ↾ 𝑆) = (𝑆 ∩ dom 𝐹) |
25 | | df-fn 6358 |
. . . . . . . . . . . 12
⊢ ((𝐹 ↾ 𝑆) Fn (𝑆 ∩ dom 𝐹) ↔ (Fun (𝐹 ↾ 𝑆) ∧ dom (𝐹 ↾ 𝑆) = (𝑆 ∩ dom 𝐹))) |
26 | 23, 24, 25 | sylanblrc 592 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹 ↾ 𝑆) Fn (𝑆 ∩ dom 𝐹)) |
27 | 26 | adantr 483 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐹 ↾ 𝑆) Fn (𝑆 ∩ dom 𝐹)) |
28 | 27 | adantr 483 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹 ↾ 𝑆) Fn (𝑆 ∩ dom 𝐹)) |
29 | | vex 3497 |
. . . . . . . . . . 11
⊢ 𝑧 ∈ V |
30 | | ovex 7189 |
. . . . . . . . . . 11
⊢ (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))) ∈ V |
31 | 29, 30 | fnsn 6412 |
. . . . . . . . . 10
⊢
{〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉} Fn {𝑧} |
32 | 31 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → {〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉} Fn {𝑧}) |
33 | | eldifn 4104 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ¬ 𝑧 ∈ dom 𝐹) |
34 | | elinel2 4173 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (𝑆 ∩ dom 𝐹) → 𝑧 ∈ dom 𝐹) |
35 | 33, 34 | nsyl 142 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ¬ 𝑧 ∈ (𝑆 ∩ dom 𝐹)) |
36 | | disjsn 4647 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ (𝑆 ∩ dom 𝐹)) |
37 | 35, 36 | sylibr 236 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅) |
38 | 37 | adantl 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅) |
39 | 38 | adantr 483 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → ((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅) |
40 | | simpr 487 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → 𝑤 ∈ (𝑆 ∩ dom 𝐹)) |
41 | | fvun1 6754 |
. . . . . . . . 9
⊢ (((𝐹 ↾ 𝑆) Fn (𝑆 ∩ dom 𝐹) ∧ {〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉} Fn {𝑧} ∧ (((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅ ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹))) → (((𝐹 ↾ 𝑆) ∪ {〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉})‘𝑤) = ((𝐹 ↾ 𝑆)‘𝑤)) |
42 | 28, 32, 39, 40, 41 | syl112anc 1370 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (((𝐹 ↾ 𝑆) ∪ {〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉})‘𝑤) = ((𝐹 ↾ 𝑆)‘𝑤)) |
43 | 20, 42 | syl5eq 2868 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶‘𝑤) = ((𝐹 ↾ 𝑆)‘𝑤)) |
44 | | elinel1 4172 |
. . . . . . . . 9
⊢ (𝑤 ∈ (𝑆 ∩ dom 𝐹) → 𝑤 ∈ 𝑆) |
45 | 44 | adantl 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → 𝑤 ∈ 𝑆) |
46 | 45 | fvresd 6690 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → ((𝐹 ↾ 𝑆)‘𝑤) = (𝐹‘𝑤)) |
47 | 43, 46 | eqtrd 2856 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶‘𝑤) = (𝐹‘𝑤)) |
48 | 6, 8, 14, 19 | frrlem11 33133 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) |
49 | | fnfun 6453 |
. . . . . . . . . . 11
⊢ (𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → Fun 𝐶) |
50 | 48, 49 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → Fun 𝐶) |
51 | 50 | adantr 483 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Fun 𝐶) |
52 | | ssun1 4148 |
. . . . . . . . . . 11
⊢ (𝐹 ↾ 𝑆) ⊆ ((𝐹 ↾ 𝑆) ∪ {〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}) |
53 | 52, 19 | sseqtrri 4004 |
. . . . . . . . . 10
⊢ (𝐹 ↾ 𝑆) ⊆ 𝐶 |
54 | 53 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹 ↾ 𝑆) ⊆ 𝐶) |
55 | | eldifi 4103 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → 𝑧 ∈ 𝐴) |
56 | | frrlem12.7 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆) |
57 | 55, 56 | sylan2 594 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆) |
58 | | rspa 3206 |
. . . . . . . . . . . 12
⊢
((∀𝑤 ∈
𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆 ∧ 𝑤 ∈ 𝑆) → Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆) |
59 | 57, 44, 58 | syl2an 597 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆) |
60 | 6, 8 | frrlem8 33130 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ dom 𝐹 → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹) |
61 | 5, 60 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ (𝑆 ∩ dom 𝐹) → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹) |
62 | 61 | adantl 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹) |
63 | 59, 62 | ssind 4209 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹)) |
64 | 63, 24 | sseqtrrdi 4018 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ dom (𝐹 ↾ 𝑆)) |
65 | | fun2ssres 6399 |
. . . . . . . . 9
⊢ ((Fun
𝐶 ∧ (𝐹 ↾ 𝑆) ⊆ 𝐶 ∧ Pred(𝑅, 𝐴, 𝑤) ⊆ dom (𝐹 ↾ 𝑆)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = ((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑤))) |
66 | 51, 54, 64, 65 | syl3anc 1367 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = ((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑤))) |
67 | 59 | resabs1d 5884 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → ((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))) |
68 | 66, 67 | eqtrd 2856 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))) |
69 | 68 | oveq2d 7172 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤)))) |
70 | 18, 47, 69 | 3eqtr4d 2866 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))) |
71 | 70 | ex 415 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑤 ∈ (𝑆 ∩ dom 𝐹) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))) |
72 | 29, 30 | fvsn 6943 |
. . . . . 6
⊢
({〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}‘𝑧) = (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))) |
73 | 19 | fveq1i 6671 |
. . . . . . 7
⊢ (𝐶‘𝑧) = (((𝐹 ↾ 𝑆) ∪ {〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉})‘𝑧) |
74 | 31 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → {〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉} Fn {𝑧}) |
75 | | vsnid 4602 |
. . . . . . . . 9
⊢ 𝑧 ∈ {𝑧} |
76 | 75 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝑧 ∈ {𝑧}) |
77 | | fvun2 6755 |
. . . . . . . 8
⊢ (((𝐹 ↾ 𝑆) Fn (𝑆 ∩ dom 𝐹) ∧ {〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉} Fn {𝑧} ∧ (((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅ ∧ 𝑧 ∈ {𝑧})) → (((𝐹 ↾ 𝑆) ∪ {〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉})‘𝑧) = ({〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}‘𝑧)) |
78 | 27, 74, 38, 76, 77 | syl112anc 1370 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (((𝐹 ↾ 𝑆) ∪ {〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉})‘𝑧) = ({〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}‘𝑧)) |
79 | 73, 78 | syl5eq 2868 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐶‘𝑧) = ({〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}‘𝑧)) |
80 | 19 | reseq1i 5849 |
. . . . . . . . 9
⊢ (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)) = (((𝐹 ↾ 𝑆) ∪ {〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}) ↾ Pred(𝑅, 𝐴, 𝑧)) |
81 | | resundir 5868 |
. . . . . . . . 9
⊢ (((𝐹 ↾ 𝑆) ∪ {〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}) ↾ Pred(𝑅, 𝐴, 𝑧)) = (((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉} ↾ Pred(𝑅, 𝐴, 𝑧))) |
82 | 80, 81 | eqtri 2844 |
. . . . . . . 8
⊢ (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)) = (((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉} ↾ Pred(𝑅, 𝐴, 𝑧))) |
83 | | frrlem12.6 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆) |
84 | 55, 83 | sylan2 594 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆) |
85 | 84 | resabs1d 5884 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))) |
86 | | frrlem12.5 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 Fr 𝐴) |
87 | | predfrirr 6177 |
. . . . . . . . . . . . 13
⊢ (𝑅 Fr 𝐴 → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧)) |
88 | 86, 87 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧)) |
89 | 88 | adantr 483 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧)) |
90 | | ressnop0 6915 |
. . . . . . . . . . 11
⊢ (¬
𝑧 ∈ Pred(𝑅, 𝐴, 𝑧) → ({〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉} ↾ Pred(𝑅, 𝐴, 𝑧)) = ∅) |
91 | 89, 90 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ({〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉} ↾ Pred(𝑅, 𝐴, 𝑧)) = ∅) |
92 | 85, 91 | uneq12d 4140 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉} ↾ Pred(𝑅, 𝐴, 𝑧))) = ((𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ∅)) |
93 | | un0 4344 |
. . . . . . . . 9
⊢ ((𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ∅) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) |
94 | 92, 93 | syl6eq 2872 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉} ↾ Pred(𝑅, 𝐴, 𝑧))) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))) |
95 | 82, 94 | syl5eq 2868 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))) |
96 | 95 | oveq2d 7172 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧))) = (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))) |
97 | 72, 79, 96 | 3eqtr4a 2882 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐶‘𝑧) = (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)))) |
98 | | fveq2 6670 |
. . . . . 6
⊢ (𝑤 = 𝑧 → (𝐶‘𝑤) = (𝐶‘𝑧)) |
99 | | id 22 |
. . . . . . 7
⊢ (𝑤 = 𝑧 → 𝑤 = 𝑧) |
100 | | predeq3 6152 |
. . . . . . . 8
⊢ (𝑤 = 𝑧 → Pred(𝑅, 𝐴, 𝑤) = Pred(𝑅, 𝐴, 𝑧)) |
101 | 100 | reseq2d 5853 |
. . . . . . 7
⊢ (𝑤 = 𝑧 → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧))) |
102 | 99, 101 | oveq12d 7174 |
. . . . . 6
⊢ (𝑤 = 𝑧 → (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))) = (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)))) |
103 | 98, 102 | eqeq12d 2837 |
. . . . 5
⊢ (𝑤 = 𝑧 → ((𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))) ↔ (𝐶‘𝑧) = (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧))))) |
104 | 97, 103 | syl5ibrcom 249 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑤 = 𝑧 → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))) |
105 | 71, 104 | jaod 855 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ((𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 = 𝑧) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))) |
106 | 4, 105 | syl5bi 244 |
. 2
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))) |
107 | 106 | 3impia 1113 |
1
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))) |