MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  frrlem12 Structured version   Visualization version   GIF version

Theorem frrlem12 8229
Description: Lemma for well-founded recursion. Next, we calculate the value of 𝐶. (Contributed by Scott Fenton, 7-Dec-2022.)
Hypotheses
Ref Expression
frrlem11.1 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
frrlem11.2 𝐹 = frecs(𝑅, 𝐴, 𝐺)
frrlem11.3 ((𝜑 ∧ (𝑔𝐵𝐵)) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣))
frrlem11.4 𝐶 = ((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})
frrlem12.5 (𝜑𝑅 Fr 𝐴)
frrlem12.6 ((𝜑𝑧𝐴) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
frrlem12.7 ((𝜑𝑧𝐴) → ∀𝑤𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
Assertion
Ref Expression
frrlem12 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) → (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
Distinct variable groups:   𝐴,𝑓,𝑥,𝑦,𝑧   𝑓,𝐺,𝑥,𝑦,𝑧   𝑅,𝑓,𝑥,𝑦,𝑧   𝐵,𝑔,,𝑧   𝑥,𝐹,𝑢,𝑣,𝑧   𝜑,𝑓,𝑧   𝑓,𝐹   𝜑,𝑔,,𝑥,𝑢,𝑣   𝐴,,𝑤,𝑓,𝑦,𝑥   𝑤,𝐺   𝑤,𝑅   𝑦,𝐹   𝑥,𝐵
Allowed substitution hints:   𝜑(𝑦,𝑤)   𝐴(𝑣,𝑢,𝑔)   𝐵(𝑦,𝑤,𝑣,𝑢,𝑓)   𝐶(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢,𝑓,𝑔,)   𝑅(𝑣,𝑢,𝑔,)   𝑆(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢,𝑓,𝑔,)   𝐹(𝑤,𝑔,)   𝐺(𝑣,𝑢,𝑔,)

Proof of Theorem frrlem12
Dummy variables 𝑝 𝑞 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elun 4109 . . . 4 (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 ∈ {𝑧}))
2 velsn 4603 . . . . 5 (𝑤 ∈ {𝑧} ↔ 𝑤 = 𝑧)
32orbi2i 912 . . . 4 ((𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 ∈ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 = 𝑧))
41, 3bitri 275 . . 3 (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 = 𝑧))
5 elinel2 4157 . . . . . . . 8 (𝑤 ∈ (𝑆 ∩ dom 𝐹) → 𝑤 ∈ dom 𝐹)
6 frrlem11.1 . . . . . . . . . 10 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
76frrlem1 8218 . . . . . . . . 9 𝐵 = {𝑝 ∣ ∃𝑞(𝑝 Fn 𝑞 ∧ (𝑞𝐴 ∧ ∀𝑤𝑞 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑞) ∧ ∀𝑤𝑞 (𝑝𝑤) = (𝑤𝐺(𝑝 ↾ Pred(𝑅, 𝐴, 𝑤))))}
8 frrlem11.2 . . . . . . . . 9 𝐹 = frecs(𝑅, 𝐴, 𝐺)
9 breq1 5109 . . . . . . . . . . . . 13 (𝑥 = 𝑞 → (𝑥𝑔𝑢𝑞𝑔𝑢))
10 breq1 5109 . . . . . . . . . . . . 13 (𝑥 = 𝑞 → (𝑥𝑣𝑞𝑣))
119, 10anbi12d 632 . . . . . . . . . . . 12 (𝑥 = 𝑞 → ((𝑥𝑔𝑢𝑥𝑣) ↔ (𝑞𝑔𝑢𝑞𝑣)))
1211imbi1d 342 . . . . . . . . . . 11 (𝑥 = 𝑞 → (((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣) ↔ ((𝑞𝑔𝑢𝑞𝑣) → 𝑢 = 𝑣)))
1312imbi2d 341 . . . . . . . . . 10 (𝑥 = 𝑞 → (((𝜑 ∧ (𝑔𝐵𝐵)) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣)) ↔ ((𝜑 ∧ (𝑔𝐵𝐵)) → ((𝑞𝑔𝑢𝑞𝑣) → 𝑢 = 𝑣))))
14 frrlem11.3 . . . . . . . . . 10 ((𝜑 ∧ (𝑔𝐵𝐵)) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣))
1513, 14chvarvv 2003 . . . . . . . . 9 ((𝜑 ∧ (𝑔𝐵𝐵)) → ((𝑞𝑔𝑢𝑞𝑣) → 𝑢 = 𝑣))
167, 8, 15frrlem10 8227 . . . . . . . 8 ((𝜑𝑤 ∈ dom 𝐹) → (𝐹𝑤) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
175, 16sylan2 594 . . . . . . 7 ((𝜑𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹𝑤) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
1817adantlr 714 . . . . . 6 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹𝑤) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
19 frrlem11.4 . . . . . . . . 9 𝐶 = ((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})
2019fveq1i 6844 . . . . . . . 8 (𝐶𝑤) = (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑤)
216, 8, 14frrlem9 8226 . . . . . . . . . . . . 13 (𝜑 → Fun 𝐹)
2221funresd 6545 . . . . . . . . . . . 12 (𝜑 → Fun (𝐹𝑆))
23 dmres 5960 . . . . . . . . . . . 12 dom (𝐹𝑆) = (𝑆 ∩ dom 𝐹)
24 df-fn 6500 . . . . . . . . . . . 12 ((𝐹𝑆) Fn (𝑆 ∩ dom 𝐹) ↔ (Fun (𝐹𝑆) ∧ dom (𝐹𝑆) = (𝑆 ∩ dom 𝐹)))
2522, 23, 24sylanblrc 591 . . . . . . . . . . 11 (𝜑 → (𝐹𝑆) Fn (𝑆 ∩ dom 𝐹))
2625adantr 482 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐹𝑆) Fn (𝑆 ∩ dom 𝐹))
2726adantr 482 . . . . . . . . 9 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹𝑆) Fn (𝑆 ∩ dom 𝐹))
28 vex 3450 . . . . . . . . . . 11 𝑧 ∈ V
29 ovex 7391 . . . . . . . . . . 11 (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))) ∈ V
3028, 29fnsn 6560 . . . . . . . . . 10 {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧}
3130a1i 11 . . . . . . . . 9 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧})
32 eldifn 4088 . . . . . . . . . . . . 13 (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ¬ 𝑧 ∈ dom 𝐹)
33 elinel2 4157 . . . . . . . . . . . . 13 (𝑧 ∈ (𝑆 ∩ dom 𝐹) → 𝑧 ∈ dom 𝐹)
3432, 33nsyl 140 . . . . . . . . . . . 12 (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ¬ 𝑧 ∈ (𝑆 ∩ dom 𝐹))
35 disjsn 4673 . . . . . . . . . . . 12 (((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ (𝑆 ∩ dom 𝐹))
3634, 35sylibr 233 . . . . . . . . . . 11 (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅)
3736adantl 483 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅)
3837adantr 482 . . . . . . . . 9 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → ((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅)
39 simpr 486 . . . . . . . . 9 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → 𝑤 ∈ (𝑆 ∩ dom 𝐹))
40 fvun1 6933 . . . . . . . . 9 (((𝐹𝑆) Fn (𝑆 ∩ dom 𝐹) ∧ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧} ∧ (((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅ ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹))) → (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑤) = ((𝐹𝑆)‘𝑤))
4127, 31, 38, 39, 40syl112anc 1375 . . . . . . . 8 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑤) = ((𝐹𝑆)‘𝑤))
4220, 41eqtrid 2789 . . . . . . 7 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶𝑤) = ((𝐹𝑆)‘𝑤))
43 elinel1 4156 . . . . . . . . 9 (𝑤 ∈ (𝑆 ∩ dom 𝐹) → 𝑤𝑆)
4443adantl 483 . . . . . . . 8 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → 𝑤𝑆)
4544fvresd 6863 . . . . . . 7 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → ((𝐹𝑆)‘𝑤) = (𝐹𝑤))
4642, 45eqtrd 2777 . . . . . 6 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶𝑤) = (𝐹𝑤))
476, 8, 14, 19frrlem11 8228 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))
48 fnfun 6603 . . . . . . . . . . 11 (𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → Fun 𝐶)
4947, 48syl 17 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → Fun 𝐶)
5049adantr 482 . . . . . . . . 9 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Fun 𝐶)
51 ssun1 4133 . . . . . . . . . . 11 (𝐹𝑆) ⊆ ((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})
5251, 19sseqtrri 3982 . . . . . . . . . 10 (𝐹𝑆) ⊆ 𝐶
5352a1i 11 . . . . . . . . 9 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹𝑆) ⊆ 𝐶)
54 eldifi 4087 . . . . . . . . . . . . 13 (𝑧 ∈ (𝐴 ∖ dom 𝐹) → 𝑧𝐴)
55 frrlem12.7 . . . . . . . . . . . . 13 ((𝜑𝑧𝐴) → ∀𝑤𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
5654, 55sylan2 594 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ∀𝑤𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
57 rspa 3232 . . . . . . . . . . . 12 ((∀𝑤𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆𝑤𝑆) → Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
5856, 43, 57syl2an 597 . . . . . . . . . . 11 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
596, 8frrlem8 8225 . . . . . . . . . . . . 13 (𝑤 ∈ dom 𝐹 → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹)
605, 59syl 17 . . . . . . . . . . . 12 (𝑤 ∈ (𝑆 ∩ dom 𝐹) → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹)
6160adantl 483 . . . . . . . . . . 11 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹)
6258, 61ssind 4193 . . . . . . . . . 10 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹))
6362, 23sseqtrrdi 3996 . . . . . . . . 9 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ dom (𝐹𝑆))
64 fun2ssres 6547 . . . . . . . . 9 ((Fun 𝐶 ∧ (𝐹𝑆) ⊆ 𝐶 ∧ Pred(𝑅, 𝐴, 𝑤) ⊆ dom (𝐹𝑆)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = ((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑤)))
6550, 53, 63, 64syl3anc 1372 . . . . . . . 8 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = ((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑤)))
6658resabs1d 5969 . . . . . . . 8 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → ((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑤)))
6765, 66eqtrd 2777 . . . . . . 7 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑤)))
6867oveq2d 7374 . . . . . 6 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
6918, 46, 683eqtr4d 2787 . . . . 5 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
7069ex 414 . . . 4 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑤 ∈ (𝑆 ∩ dom 𝐹) → (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
7128, 29fvsn 7128 . . . . . 6 ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧) = (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
7219fveq1i 6844 . . . . . . 7 (𝐶𝑧) = (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑧)
7330a1i 11 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧})
74 vsnid 4624 . . . . . . . . 9 𝑧 ∈ {𝑧}
7574a1i 11 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝑧 ∈ {𝑧})
76 fvun2 6934 . . . . . . . 8 (((𝐹𝑆) Fn (𝑆 ∩ dom 𝐹) ∧ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧} ∧ (((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅ ∧ 𝑧 ∈ {𝑧})) → (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑧) = ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧))
7726, 73, 37, 75, 76syl112anc 1375 . . . . . . 7 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑧) = ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧))
7872, 77eqtrid 2789 . . . . . 6 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐶𝑧) = ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧))
7919reseq1i 5934 . . . . . . . . 9 (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)) = (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ↾ Pred(𝑅, 𝐴, 𝑧))
80 resundir 5953 . . . . . . . . 9 (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ↾ Pred(𝑅, 𝐴, 𝑧)) = (((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)))
8179, 80eqtri 2765 . . . . . . . 8 (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)) = (((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)))
82 frrlem12.6 . . . . . . . . . . . 12 ((𝜑𝑧𝐴) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
8354, 82sylan2 594 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
8483resabs1d 5969 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
85 frrlem12.5 . . . . . . . . . . . . 13 (𝜑𝑅 Fr 𝐴)
86 predfrirr 6289 . . . . . . . . . . . . 13 (𝑅 Fr 𝐴 → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧))
8785, 86syl 17 . . . . . . . . . . . 12 (𝜑 → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧))
8887adantr 482 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧))
89 ressnop0 7100 . . . . . . . . . . 11 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧) → ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)) = ∅)
9088, 89syl 17 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)) = ∅)
9184, 90uneq12d 4125 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧))) = ((𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ∅))
92 un0 4351 . . . . . . . . 9 ((𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ∅) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))
9391, 92eqtrdi 2793 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧))) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
9481, 93eqtrid 2789 . . . . . . 7 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
9594oveq2d 7374 . . . . . 6 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧))) = (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))))
9671, 78, 953eqtr4a 2803 . . . . 5 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐶𝑧) = (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧))))
97 fveq2 6843 . . . . . 6 (𝑤 = 𝑧 → (𝐶𝑤) = (𝐶𝑧))
98 id 22 . . . . . . 7 (𝑤 = 𝑧𝑤 = 𝑧)
99 predeq3 6258 . . . . . . . 8 (𝑤 = 𝑧 → Pred(𝑅, 𝐴, 𝑤) = Pred(𝑅, 𝐴, 𝑧))
10099reseq2d 5938 . . . . . . 7 (𝑤 = 𝑧 → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)))
10198, 100oveq12d 7376 . . . . . 6 (𝑤 = 𝑧 → (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))) = (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧))))
10297, 101eqeq12d 2753 . . . . 5 (𝑤 = 𝑧 → ((𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))) ↔ (𝐶𝑧) = (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)))))
10396, 102syl5ibrcom 247 . . . 4 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑤 = 𝑧 → (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
10470, 103jaod 858 . . 3 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ((𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 = 𝑧) → (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
1054, 104biimtrid 241 . 2 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
1061053impia 1118 1 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) → (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397  wo 846  w3a 1088   = wceq 1542  wex 1782  wcel 2107  {cab 2714  wral 3065  cdif 3908  cun 3909  cin 3910  wss 3911  c0 4283  {csn 4587  cop 4593   class class class wbr 5106   Fr wfr 5586  dom cdm 5634  cres 5636  Predcpred 6253  Fun wfun 6491   Fn wfn 6492  cfv 6497  (class class class)co 7358  frecscfrecs 8212
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-id 5532  df-fr 5589  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-iota 6449  df-fun 6499  df-fn 6500  df-fv 6505  df-ov 7361  df-frecs 8213
This theorem is referenced by:  frrlem13  8230
  Copyright terms: Public domain W3C validator