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

Theorem frrlem12 8284
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 4148 . . . 4 (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 ∈ {𝑧}))
2 velsn 4644 . . . . 5 (𝑤 ∈ {𝑧} ↔ 𝑤 = 𝑧)
32orbi2i 911 . . . 4 ((𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 ∈ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 = 𝑧))
41, 3bitri 274 . . 3 (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 = 𝑧))
5 elinel2 4196 . . . . . . . 8 (𝑤 ∈ (𝑆 ∩ dom 𝐹) → 𝑤 ∈ dom 𝐹)
6 frrlem11.1 . . . . . . . . . 10 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
76frrlem1 8273 . . . . . . . . 9 𝐵 = {𝑝 ∣ ∃𝑞(𝑝 Fn 𝑞 ∧ (𝑞𝐴 ∧ ∀𝑤𝑞 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑞) ∧ ∀𝑤𝑞 (𝑝𝑤) = (𝑤𝐺(𝑝 ↾ Pred(𝑅, 𝐴, 𝑤))))}
8 frrlem11.2 . . . . . . . . 9 𝐹 = frecs(𝑅, 𝐴, 𝐺)
9 breq1 5151 . . . . . . . . . . . . 13 (𝑥 = 𝑞 → (𝑥𝑔𝑢𝑞𝑔𝑢))
10 breq1 5151 . . . . . . . . . . . . 13 (𝑥 = 𝑞 → (𝑥𝑣𝑞𝑣))
119, 10anbi12d 631 . . . . . . . . . . . 12 (𝑥 = 𝑞 → ((𝑥𝑔𝑢𝑥𝑣) ↔ (𝑞𝑔𝑢𝑞𝑣)))
1211imbi1d 341 . . . . . . . . . . 11 (𝑥 = 𝑞 → (((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣) ↔ ((𝑞𝑔𝑢𝑞𝑣) → 𝑢 = 𝑣)))
1312imbi2d 340 . . . . . . . . . 10 (𝑥 = 𝑞 → (((𝜑 ∧ (𝑔𝐵𝐵)) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣)) ↔ ((𝜑 ∧ (𝑔𝐵𝐵)) → ((𝑞𝑔𝑢𝑞𝑣) → 𝑢 = 𝑣))))
14 frrlem11.3 . . . . . . . . . 10 ((𝜑 ∧ (𝑔𝐵𝐵)) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣))
1513, 14chvarvv 2002 . . . . . . . . 9 ((𝜑 ∧ (𝑔𝐵𝐵)) → ((𝑞𝑔𝑢𝑞𝑣) → 𝑢 = 𝑣))
167, 8, 15frrlem10 8282 . . . . . . . 8 ((𝜑𝑤 ∈ dom 𝐹) → (𝐹𝑤) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
175, 16sylan2 593 . . . . . . 7 ((𝜑𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹𝑤) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
1817adantlr 713 . . . . . 6 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹𝑤) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
19 frrlem11.4 . . . . . . . . 9 𝐶 = ((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})
2019fveq1i 6892 . . . . . . . 8 (𝐶𝑤) = (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑤)
216, 8, 14frrlem9 8281 . . . . . . . . . . . . 13 (𝜑 → Fun 𝐹)
2221funresd 6591 . . . . . . . . . . . 12 (𝜑 → Fun (𝐹𝑆))
23 dmres 6003 . . . . . . . . . . . 12 dom (𝐹𝑆) = (𝑆 ∩ dom 𝐹)
24 df-fn 6546 . . . . . . . . . . . 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 3478 . . . . . . . . . . 11 𝑧 ∈ V
29 ovex 7444 . . . . . . . . . . 11 (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))) ∈ V
3028, 29fnsn 6606 . . . . . . . . . 10 {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧}
3130a1i 11 . . . . . . . . 9 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧})
32 eldifn 4127 . . . . . . . . . . . . 13 (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ¬ 𝑧 ∈ dom 𝐹)
33 elinel2 4196 . . . . . . . . . . . . 13 (𝑧 ∈ (𝑆 ∩ dom 𝐹) → 𝑧 ∈ dom 𝐹)
3432, 33nsyl 140 . . . . . . . . . . . 12 (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ¬ 𝑧 ∈ (𝑆 ∩ dom 𝐹))
35 disjsn 4715 . . . . . . . . . . . 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 6982 . . . . . . . . 9 (((𝐹𝑆) Fn (𝑆 ∩ dom 𝐹) ∧ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧} ∧ (((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅ ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹))) → (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑤) = ((𝐹𝑆)‘𝑤))
4127, 31, 38, 39, 40syl112anc 1374 . . . . . . . 8 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑤) = ((𝐹𝑆)‘𝑤))
4220, 41eqtrid 2784 . . . . . . 7 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶𝑤) = ((𝐹𝑆)‘𝑤))
43 elinel1 4195 . . . . . . . . 9 (𝑤 ∈ (𝑆 ∩ dom 𝐹) → 𝑤𝑆)
4443adantl 482 . . . . . . . 8 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → 𝑤𝑆)
4544fvresd 6911 . . . . . . 7 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → ((𝐹𝑆)‘𝑤) = (𝐹𝑤))
4642, 45eqtrd 2772 . . . . . 6 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶𝑤) = (𝐹𝑤))
476, 8, 14, 19frrlem11 8283 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))
48 fnfun 6649 . . . . . . . . . . 11 (𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → Fun 𝐶)
4947, 48syl 17 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → Fun 𝐶)
5049adantr 481 . . . . . . . . 9 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Fun 𝐶)
51 ssun1 4172 . . . . . . . . . . 11 (𝐹𝑆) ⊆ ((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})
5251, 19sseqtrri 4019 . . . . . . . . . 10 (𝐹𝑆) ⊆ 𝐶
5352a1i 11 . . . . . . . . 9 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹𝑆) ⊆ 𝐶)
54 eldifi 4126 . . . . . . . . . . . . 13 (𝑧 ∈ (𝐴 ∖ dom 𝐹) → 𝑧𝐴)
55 frrlem12.7 . . . . . . . . . . . . 13 ((𝜑𝑧𝐴) → ∀𝑤𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
5654, 55sylan2 593 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ∀𝑤𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
57 rspa 3245 . . . . . . . . . . . 12 ((∀𝑤𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆𝑤𝑆) → Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
5856, 43, 57syl2an 596 . . . . . . . . . . 11 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
596, 8frrlem8 8280 . . . . . . . . . . . . 13 (𝑤 ∈ dom 𝐹 → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹)
605, 59syl 17 . . . . . . . . . . . 12 (𝑤 ∈ (𝑆 ∩ dom 𝐹) → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹)
6160adantl 482 . . . . . . . . . . 11 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹)
6258, 61ssind 4232 . . . . . . . . . 10 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹))
6362, 23sseqtrrdi 4033 . . . . . . . . 9 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ dom (𝐹𝑆))
64 fun2ssres 6593 . . . . . . . . 9 ((Fun 𝐶 ∧ (𝐹𝑆) ⊆ 𝐶 ∧ Pred(𝑅, 𝐴, 𝑤) ⊆ dom (𝐹𝑆)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = ((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑤)))
6550, 53, 63, 64syl3anc 1371 . . . . . . . 8 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = ((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑤)))
6658resabs1d 6012 . . . . . . . 8 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → ((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑤)))
6765, 66eqtrd 2772 . . . . . . 7 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑤)))
6867oveq2d 7427 . . . . . 6 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
6918, 46, 683eqtr4d 2782 . . . . 5 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
7069ex 413 . . . 4 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑤 ∈ (𝑆 ∩ dom 𝐹) → (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
7128, 29fvsn 7181 . . . . . 6 ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧) = (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
7219fveq1i 6892 . . . . . . 7 (𝐶𝑧) = (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑧)
7330a1i 11 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧})
74 vsnid 4665 . . . . . . . . 9 𝑧 ∈ {𝑧}
7574a1i 11 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝑧 ∈ {𝑧})
76 fvun2 6983 . . . . . . . 8 (((𝐹𝑆) Fn (𝑆 ∩ dom 𝐹) ∧ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧} ∧ (((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅ ∧ 𝑧 ∈ {𝑧})) → (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑧) = ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧))
7726, 73, 37, 75, 76syl112anc 1374 . . . . . . 7 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑧) = ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧))
7872, 77eqtrid 2784 . . . . . 6 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐶𝑧) = ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧))
7919reseq1i 5977 . . . . . . . . 9 (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)) = (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ↾ Pred(𝑅, 𝐴, 𝑧))
80 resundir 5996 . . . . . . . . 9 (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ↾ Pred(𝑅, 𝐴, 𝑧)) = (((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)))
8179, 80eqtri 2760 . . . . . . . 8 (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)) = (((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)))
82 frrlem12.6 . . . . . . . . . . . 12 ((𝜑𝑧𝐴) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
8354, 82sylan2 593 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
8483resabs1d 6012 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
85 frrlem12.5 . . . . . . . . . . . . 13 (𝜑𝑅 Fr 𝐴)
86 predfrirr 6335 . . . . . . . . . . . . 13 (𝑅 Fr 𝐴 → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧))
8785, 86syl 17 . . . . . . . . . . . 12 (𝜑 → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧))
8887adantr 481 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧))
89 ressnop0 7153 . . . . . . . . . . 11 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧) → ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)) = ∅)
9088, 89syl 17 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)) = ∅)
9184, 90uneq12d 4164 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧))) = ((𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ∅))
92 un0 4390 . . . . . . . . 9 ((𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ∅) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))
9391, 92eqtrdi 2788 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧))) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
9481, 93eqtrid 2784 . . . . . . 7 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
9594oveq2d 7427 . . . . . 6 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧))) = (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))))
9671, 78, 953eqtr4a 2798 . . . . 5 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐶𝑧) = (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧))))
97 fveq2 6891 . . . . . 6 (𝑤 = 𝑧 → (𝐶𝑤) = (𝐶𝑧))
98 id 22 . . . . . . 7 (𝑤 = 𝑧𝑤 = 𝑧)
99 predeq3 6304 . . . . . . . 8 (𝑤 = 𝑧 → Pred(𝑅, 𝐴, 𝑤) = Pred(𝑅, 𝐴, 𝑧))
10099reseq2d 5981 . . . . . . 7 (𝑤 = 𝑧 → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)))
10198, 100oveq12d 7429 . . . . . 6 (𝑤 = 𝑧 → (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))) = (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧))))
10297, 101eqeq12d 2748 . . . . 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 2709  wral 3061  cdif 3945  cun 3946  cin 3947  wss 3948  c0 4322  {csn 4628  cop 4634   class class class wbr 5148   Fr wfr 5628  dom cdm 5676  cres 5678  Predcpred 6299  Fun wfun 6537   Fn wfn 6538  cfv 6543  (class class class)co 7411  frecscfrecs 8267
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 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427
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 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-id 5574  df-fr 5631  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-iota 6495  df-fun 6545  df-fn 6546  df-fv 6551  df-ov 7414  df-frecs 8268
This theorem is referenced by:  frrlem13  8285
  Copyright terms: Public domain W3C validator