| Step | Hyp | Ref
| Expression |
| 1 | | vex 3484 |
. . . 4
⊢ 𝑦 ∈ V |
| 2 | 1 | eldm2 5912 |
. . 3
⊢ (𝑦 ∈ dom 𝐹 ↔ ∃𝑧〈𝑦, 𝑧〉 ∈ 𝐹) |
| 3 | | frrlem9.1 |
. . . . . . . . 9
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} |
| 4 | | frrlem9.2 |
. . . . . . . . 9
⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) |
| 5 | 3, 4 | frrlem5 8315 |
. . . . . . . 8
⊢ 𝐹 = ∪
𝐵 |
| 6 | 3 | unieqi 4919 |
. . . . . . . 8
⊢ ∪ 𝐵 =
∪ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} |
| 7 | 5, 6 | eqtri 2765 |
. . . . . . 7
⊢ 𝐹 = ∪
{𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} |
| 8 | 7 | eleq2i 2833 |
. . . . . 6
⊢
(〈𝑦, 𝑧〉 ∈ 𝐹 ↔ 〈𝑦, 𝑧〉 ∈ ∪
{𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}) |
| 9 | | eluniab 4921 |
. . . . . 6
⊢
(〈𝑦, 𝑧〉 ∈ ∪ {𝑓
∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ↔ ∃𝑓(〈𝑦, 𝑧〉 ∈ 𝑓 ∧ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))))) |
| 10 | 8, 9 | bitri 275 |
. . . . 5
⊢
(〈𝑦, 𝑧〉 ∈ 𝐹 ↔ ∃𝑓(〈𝑦, 𝑧〉 ∈ 𝑓 ∧ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))))) |
| 11 | | 19.8a 2181 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) → ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))) |
| 12 | 11 | 3ad2ant2 1135 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ 〈𝑦, 𝑧〉 ∈ 𝑓) → ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))) |
| 13 | | abid 2718 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ↔ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))) |
| 14 | 12, 13 | sylibr 234 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ 〈𝑦, 𝑧〉 ∈ 𝑓) → 𝑓 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}) |
| 15 | | elssuni 4937 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} → 𝑓 ⊆ ∪ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}) |
| 16 | 14, 15 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ 〈𝑦, 𝑧〉 ∈ 𝑓) → 𝑓 ⊆ ∪ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}) |
| 17 | 16, 7 | sseqtrrdi 4025 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ 〈𝑦, 𝑧〉 ∈ 𝑓) → 𝑓 ⊆ 𝐹) |
| 18 | | simpl23 1254 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ 〈𝑦, 𝑧〉 ∈ 𝑓) ∧ 𝑓 ⊆ 𝐹) → ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) |
| 19 | | simpl3 1194 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ 〈𝑦, 𝑧〉 ∈ 𝑓) ∧ 𝑓 ⊆ 𝐹) → 〈𝑦, 𝑧〉 ∈ 𝑓) |
| 20 | | vex 3484 |
. . . . . . . . . . . . . . 15
⊢ 𝑧 ∈ V |
| 21 | 1, 20 | opeldm 5918 |
. . . . . . . . . . . . . 14
⊢
(〈𝑦, 𝑧〉 ∈ 𝑓 → 𝑦 ∈ dom 𝑓) |
| 22 | 19, 21 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ 〈𝑦, 𝑧〉 ∈ 𝑓) ∧ 𝑓 ⊆ 𝐹) → 𝑦 ∈ dom 𝑓) |
| 23 | | simpl21 1252 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ 〈𝑦, 𝑧〉 ∈ 𝑓) ∧ 𝑓 ⊆ 𝐹) → 𝑓 Fn 𝑥) |
| 24 | 23 | fndmd 6673 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ 〈𝑦, 𝑧〉 ∈ 𝑓) ∧ 𝑓 ⊆ 𝐹) → dom 𝑓 = 𝑥) |
| 25 | 22, 24 | eleqtrd 2843 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ 〈𝑦, 𝑧〉 ∈ 𝑓) ∧ 𝑓 ⊆ 𝐹) → 𝑦 ∈ 𝑥) |
| 26 | | rsp 3247 |
. . . . . . . . . . . 12
⊢
(∀𝑦 ∈
𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) → (𝑦 ∈ 𝑥 → (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))) |
| 27 | 18, 25, 26 | sylc 65 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ 〈𝑦, 𝑧〉 ∈ 𝑓) ∧ 𝑓 ⊆ 𝐹) → (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) |
| 28 | | simpl1 1192 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ 〈𝑦, 𝑧〉 ∈ 𝑓) ∧ 𝑓 ⊆ 𝐹) → 𝜑) |
| 29 | | frrlem9.3 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) |
| 30 | 3, 4, 29 | frrlem9 8319 |
. . . . . . . . . . . . 13
⊢ (𝜑 → Fun 𝐹) |
| 31 | 28, 30 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ 〈𝑦, 𝑧〉 ∈ 𝑓) ∧ 𝑓 ⊆ 𝐹) → Fun 𝐹) |
| 32 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ 〈𝑦, 𝑧〉 ∈ 𝑓) ∧ 𝑓 ⊆ 𝐹) → 𝑓 ⊆ 𝐹) |
| 33 | | funssfv 6927 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐹 ∧ 𝑓 ⊆ 𝐹 ∧ 𝑦 ∈ dom 𝑓) → (𝐹‘𝑦) = (𝑓‘𝑦)) |
| 34 | 31, 32, 22, 33 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ 〈𝑦, 𝑧〉 ∈ 𝑓) ∧ 𝑓 ⊆ 𝐹) → (𝐹‘𝑦) = (𝑓‘𝑦)) |
| 35 | | simp22r 1294 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ 〈𝑦, 𝑧〉 ∈ 𝑓) → ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) |
| 36 | 35 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ 〈𝑦, 𝑧〉 ∈ 𝑓) ∧ 𝑓 ⊆ 𝐹) → ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) |
| 37 | | rsp 3247 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑦 ∈
𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥 → (𝑦 ∈ 𝑥 → Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥)) |
| 38 | 36, 25, 37 | sylc 65 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ 〈𝑦, 𝑧〉 ∈ 𝑓) ∧ 𝑓 ⊆ 𝐹) → Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) |
| 39 | 38, 24 | sseqtrrd 4021 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ 〈𝑦, 𝑧〉 ∈ 𝑓) ∧ 𝑓 ⊆ 𝐹) → Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝑓) |
| 40 | | fun2ssres 6611 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝐹 ∧ 𝑓 ⊆ 𝐹 ∧ Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝑓) → (𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)) = (𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) |
| 41 | 31, 32, 39, 40 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ 〈𝑦, 𝑧〉 ∈ 𝑓) ∧ 𝑓 ⊆ 𝐹) → (𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)) = (𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) |
| 42 | 41 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ 〈𝑦, 𝑧〉 ∈ 𝑓) ∧ 𝑓 ⊆ 𝐹) → (𝑦𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) |
| 43 | 27, 34, 42 | 3eqtr4d 2787 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ 〈𝑦, 𝑧〉 ∈ 𝑓) ∧ 𝑓 ⊆ 𝐹) → (𝐹‘𝑦) = (𝑦𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))) |
| 44 | 17, 43 | mpdan 687 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ 〈𝑦, 𝑧〉 ∈ 𝑓) → (𝐹‘𝑦) = (𝑦𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))) |
| 45 | 44 | 3exp 1120 |
. . . . . . . 8
⊢ (𝜑 → ((𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) → (〈𝑦, 𝑧〉 ∈ 𝑓 → (𝐹‘𝑦) = (𝑦𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))))) |
| 46 | 45 | exlimdv 1933 |
. . . . . . 7
⊢ (𝜑 → (∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) → (〈𝑦, 𝑧〉 ∈ 𝑓 → (𝐹‘𝑦) = (𝑦𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))))) |
| 47 | 46 | impcomd 411 |
. . . . . 6
⊢ (𝜑 → ((〈𝑦, 𝑧〉 ∈ 𝑓 ∧ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))) → (𝐹‘𝑦) = (𝑦𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))) |
| 48 | 47 | exlimdv 1933 |
. . . . 5
⊢ (𝜑 → (∃𝑓(〈𝑦, 𝑧〉 ∈ 𝑓 ∧ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))) → (𝐹‘𝑦) = (𝑦𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))) |
| 49 | 10, 48 | biimtrid 242 |
. . . 4
⊢ (𝜑 → (〈𝑦, 𝑧〉 ∈ 𝐹 → (𝐹‘𝑦) = (𝑦𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))) |
| 50 | 49 | exlimdv 1933 |
. . 3
⊢ (𝜑 → (∃𝑧〈𝑦, 𝑧〉 ∈ 𝐹 → (𝐹‘𝑦) = (𝑦𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))) |
| 51 | 2, 50 | biimtrid 242 |
. 2
⊢ (𝜑 → (𝑦 ∈ dom 𝐹 → (𝐹‘𝑦) = (𝑦𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))) |
| 52 | 51 | imp 406 |
1
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐹) → (𝐹‘𝑦) = (𝑦𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))) |