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

Theorem frrlem12 8228
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 4108 . . . 4 (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 ∈ {𝑧}))
2 velsn 4602 . . . . 5 (𝑤 ∈ {𝑧} ↔ 𝑤 = 𝑧)
32orbi2i 911 . . . 4 ((𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 ∈ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 = 𝑧))
41, 3bitri 274 . . 3 (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 = 𝑧))
5 elinel2 4156 . . . . . . . 8 (𝑤 ∈ (𝑆 ∩ dom 𝐹) → 𝑤 ∈ dom 𝐹)
6 frrlem11.1 . . . . . . . . . 10 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
76frrlem1 8217 . . . . . . . . 9 𝐵 = {𝑝 ∣ ∃𝑞(𝑝 Fn 𝑞 ∧ (𝑞𝐴 ∧ ∀𝑤𝑞 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑞) ∧ ∀𝑤𝑞 (𝑝𝑤) = (𝑤𝐺(𝑝 ↾ Pred(𝑅, 𝐴, 𝑤))))}
8 frrlem11.2 . . . . . . . . 9 𝐹 = frecs(𝑅, 𝐴, 𝐺)
9 breq1 5108 . . . . . . . . . . . . 13 (𝑥 = 𝑞 → (𝑥𝑔𝑢𝑞𝑔𝑢))
10 breq1 5108 . . . . . . . . . . . . 13 (𝑥 = 𝑞 → (𝑥𝑣𝑞𝑣))
119, 10anbi12d 631 . . . . . . . . . . . 12 (𝑥 = 𝑞 → ((𝑥𝑔𝑢𝑥𝑣) ↔ (𝑞𝑔𝑢𝑞𝑣)))
1211imbi1d 341 . . . . . . . . . . 11 (𝑥 = 𝑞 → (((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣) ↔ ((𝑞𝑔𝑢𝑞𝑣) → 𝑢 = 𝑣)))
1312imbi2d 340 . . . . . . . . . 10 (𝑥 = 𝑞 → (((𝜑 ∧ (𝑔𝐵𝐵)) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣)) ↔ ((𝜑 ∧ (𝑔𝐵𝐵)) → ((𝑞𝑔𝑢𝑞𝑣) → 𝑢 = 𝑣))))
14 frrlem11.3 . . . . . . . . . 10 ((𝜑 ∧ (𝑔𝐵𝐵)) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣))
1513, 14chvarvv 2002 . . . . . . . . 9 ((𝜑 ∧ (𝑔𝐵𝐵)) → ((𝑞𝑔𝑢𝑞𝑣) → 𝑢 = 𝑣))
167, 8, 15frrlem10 8226 . . . . . . . 8 ((𝜑𝑤 ∈ dom 𝐹) → (𝐹𝑤) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
175, 16sylan2 593 . . . . . . 7 ((𝜑𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹𝑤) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
1817adantlr 713 . . . . . 6 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹𝑤) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
19 frrlem11.4 . . . . . . . . 9 𝐶 = ((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})
2019fveq1i 6843 . . . . . . . 8 (𝐶𝑤) = (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑤)
216, 8, 14frrlem9 8225 . . . . . . . . . . . . 13 (𝜑 → Fun 𝐹)
2221funresd 6544 . . . . . . . . . . . 12 (𝜑 → Fun (𝐹𝑆))
23 dmres 5959 . . . . . . . . . . . 12 dom (𝐹𝑆) = (𝑆 ∩ dom 𝐹)
24 df-fn 6499 . . . . . . . . . . . 12 ((𝐹𝑆) Fn (𝑆 ∩ dom 𝐹) ↔ (Fun (𝐹𝑆) ∧ dom (𝐹𝑆) = (𝑆 ∩ dom 𝐹)))
2522, 23, 24sylanblrc 590 . . . . . . . . . . 11 (𝜑 → (𝐹𝑆) Fn (𝑆 ∩ dom 𝐹))
2625adantr 481 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐹𝑆) Fn (𝑆 ∩ dom 𝐹))
2726adantr 481 . . . . . . . . 9 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹𝑆) Fn (𝑆 ∩ dom 𝐹))
28 vex 3449 . . . . . . . . . . 11 𝑧 ∈ V
29 ovex 7390 . . . . . . . . . . 11 (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))) ∈ V
3028, 29fnsn 6559 . . . . . . . . . 10 {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧}
3130a1i 11 . . . . . . . . 9 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧})
32 eldifn 4087 . . . . . . . . . . . . 13 (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ¬ 𝑧 ∈ dom 𝐹)
33 elinel2 4156 . . . . . . . . . . . . 13 (𝑧 ∈ (𝑆 ∩ dom 𝐹) → 𝑧 ∈ dom 𝐹)
3432, 33nsyl 140 . . . . . . . . . . . 12 (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ¬ 𝑧 ∈ (𝑆 ∩ dom 𝐹))
35 disjsn 4672 . . . . . . . . . . . 12 (((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ (𝑆 ∩ dom 𝐹))
3634, 35sylibr 233 . . . . . . . . . . 11 (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅)
3736adantl 482 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅)
3837adantr 481 . . . . . . . . 9 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → ((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅)
39 simpr 485 . . . . . . . . 9 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → 𝑤 ∈ (𝑆 ∩ dom 𝐹))
40 fvun1 6932 . . . . . . . . 9 (((𝐹𝑆) Fn (𝑆 ∩ dom 𝐹) ∧ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧} ∧ (((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅ ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹))) → (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑤) = ((𝐹𝑆)‘𝑤))
4127, 31, 38, 39, 40syl112anc 1374 . . . . . . . 8 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑤) = ((𝐹𝑆)‘𝑤))
4220, 41eqtrid 2788 . . . . . . 7 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶𝑤) = ((𝐹𝑆)‘𝑤))
43 elinel1 4155 . . . . . . . . 9 (𝑤 ∈ (𝑆 ∩ dom 𝐹) → 𝑤𝑆)
4443adantl 482 . . . . . . . 8 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → 𝑤𝑆)
4544fvresd 6862 . . . . . . 7 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → ((𝐹𝑆)‘𝑤) = (𝐹𝑤))
4642, 45eqtrd 2776 . . . . . 6 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶𝑤) = (𝐹𝑤))
476, 8, 14, 19frrlem11 8227 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))
48 fnfun 6602 . . . . . . . . . . 11 (𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → Fun 𝐶)
4947, 48syl 17 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → Fun 𝐶)
5049adantr 481 . . . . . . . . 9 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Fun 𝐶)
51 ssun1 4132 . . . . . . . . . . 11 (𝐹𝑆) ⊆ ((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})
5251, 19sseqtrri 3981 . . . . . . . . . 10 (𝐹𝑆) ⊆ 𝐶
5352a1i 11 . . . . . . . . 9 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹𝑆) ⊆ 𝐶)
54 eldifi 4086 . . . . . . . . . . . . 13 (𝑧 ∈ (𝐴 ∖ dom 𝐹) → 𝑧𝐴)
55 frrlem12.7 . . . . . . . . . . . . 13 ((𝜑𝑧𝐴) → ∀𝑤𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
5654, 55sylan2 593 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ∀𝑤𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
57 rspa 3231 . . . . . . . . . . . 12 ((∀𝑤𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆𝑤𝑆) → Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
5856, 43, 57syl2an 596 . . . . . . . . . . 11 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
596, 8frrlem8 8224 . . . . . . . . . . . . 13 (𝑤 ∈ dom 𝐹 → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹)
605, 59syl 17 . . . . . . . . . . . 12 (𝑤 ∈ (𝑆 ∩ dom 𝐹) → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹)
6160adantl 482 . . . . . . . . . . 11 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹)
6258, 61ssind 4192 . . . . . . . . . 10 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹))
6362, 23sseqtrrdi 3995 . . . . . . . . 9 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ dom (𝐹𝑆))
64 fun2ssres 6546 . . . . . . . . 9 ((Fun 𝐶 ∧ (𝐹𝑆) ⊆ 𝐶 ∧ Pred(𝑅, 𝐴, 𝑤) ⊆ dom (𝐹𝑆)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = ((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑤)))
6550, 53, 63, 64syl3anc 1371 . . . . . . . 8 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = ((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑤)))
6658resabs1d 5968 . . . . . . . 8 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → ((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑤)))
6765, 66eqtrd 2776 . . . . . . 7 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑤)))
6867oveq2d 7373 . . . . . 6 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
6918, 46, 683eqtr4d 2786 . . . . 5 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
7069ex 413 . . . 4 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑤 ∈ (𝑆 ∩ dom 𝐹) → (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
7128, 29fvsn 7127 . . . . . 6 ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧) = (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
7219fveq1i 6843 . . . . . . 7 (𝐶𝑧) = (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑧)
7330a1i 11 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧})
74 vsnid 4623 . . . . . . . . 9 𝑧 ∈ {𝑧}
7574a1i 11 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝑧 ∈ {𝑧})
76 fvun2 6933 . . . . . . . 8 (((𝐹𝑆) Fn (𝑆 ∩ dom 𝐹) ∧ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧} ∧ (((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅ ∧ 𝑧 ∈ {𝑧})) → (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑧) = ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧))
7726, 73, 37, 75, 76syl112anc 1374 . . . . . . 7 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑧) = ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧))
7872, 77eqtrid 2788 . . . . . 6 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐶𝑧) = ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧))
7919reseq1i 5933 . . . . . . . . 9 (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)) = (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ↾ Pred(𝑅, 𝐴, 𝑧))
80 resundir 5952 . . . . . . . . 9 (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ↾ Pred(𝑅, 𝐴, 𝑧)) = (((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)))
8179, 80eqtri 2764 . . . . . . . 8 (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)) = (((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)))
82 frrlem12.6 . . . . . . . . . . . 12 ((𝜑𝑧𝐴) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
8354, 82sylan2 593 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
8483resabs1d 5968 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
85 frrlem12.5 . . . . . . . . . . . . 13 (𝜑𝑅 Fr 𝐴)
86 predfrirr 6288 . . . . . . . . . . . . 13 (𝑅 Fr 𝐴 → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧))
8785, 86syl 17 . . . . . . . . . . . 12 (𝜑 → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧))
8887adantr 481 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧))
89 ressnop0 7099 . . . . . . . . . . 11 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧) → ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)) = ∅)
9088, 89syl 17 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)) = ∅)
9184, 90uneq12d 4124 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧))) = ((𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ∅))
92 un0 4350 . . . . . . . . 9 ((𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ∅) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))
9391, 92eqtrdi 2792 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧))) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
9481, 93eqtrid 2788 . . . . . . 7 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
9594oveq2d 7373 . . . . . 6 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧))) = (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))))
9671, 78, 953eqtr4a 2802 . . . . 5 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐶𝑧) = (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧))))
97 fveq2 6842 . . . . . 6 (𝑤 = 𝑧 → (𝐶𝑤) = (𝐶𝑧))
98 id 22 . . . . . . 7 (𝑤 = 𝑧𝑤 = 𝑧)
99 predeq3 6257 . . . . . . . 8 (𝑤 = 𝑧 → Pred(𝑅, 𝐴, 𝑤) = Pred(𝑅, 𝐴, 𝑧))
10099reseq2d 5937 . . . . . . 7 (𝑤 = 𝑧 → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)))
10198, 100oveq12d 7375 . . . . . 6 (𝑤 = 𝑧 → (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))) = (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧))))
10297, 101eqeq12d 2752 . . . . 5 (𝑤 = 𝑧 → ((𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))) ↔ (𝐶𝑧) = (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)))))
10396, 102syl5ibrcom 246 . . . 4 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑤 = 𝑧 → (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
10470, 103jaod 857 . . 3 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ((𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 = 𝑧) → (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
1054, 104biimtrid 241 . 2 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
1061053impia 1117 1 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) → (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wo 845  w3a 1087   = wceq 1541  wex 1781  wcel 2106  {cab 2713  wral 3064  cdif 3907  cun 3908  cin 3909  wss 3910  c0 4282  {csn 4586  cop 4592   class class class wbr 5105   Fr wfr 5585  dom cdm 5633  cres 5635  Predcpred 6252  Fun wfun 6490   Fn wfn 6491  cfv 6496  (class class class)co 7357  frecscfrecs 8211
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-id 5531  df-fr 5588  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-iota 6448  df-fun 6498  df-fn 6499  df-fv 6504  df-ov 7360  df-frecs 8212
This theorem is referenced by:  frrlem13  8229
  Copyright terms: Public domain W3C validator