Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  frrlem12 Structured version   Visualization version   GIF version

Theorem frrlem12 33247
 Description: Lemma for 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 4076 . . . 4 (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 ∈ {𝑧}))
2 velsn 4541 . . . . 5 (𝑤 ∈ {𝑧} ↔ 𝑤 = 𝑧)
32orbi2i 910 . . . 4 ((𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 ∈ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 = 𝑧))
41, 3bitri 278 . . 3 (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 = 𝑧))
5 elinel2 4123 . . . . . . . 8 (𝑤 ∈ (𝑆 ∩ dom 𝐹) → 𝑤 ∈ dom 𝐹)
6 frrlem11.1 . . . . . . . . . 10 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
76frrlem1 33236 . . . . . . . . 9 𝐵 = {𝑝 ∣ ∃𝑞(𝑝 Fn 𝑞 ∧ (𝑞𝐴 ∧ ∀𝑤𝑞 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑞) ∧ ∀𝑤𝑞 (𝑝𝑤) = (𝑤𝐺(𝑝 ↾ Pred(𝑅, 𝐴, 𝑤))))}
8 frrlem11.2 . . . . . . . . 9 𝐹 = frecs(𝑅, 𝐴, 𝐺)
9 breq1 5033 . . . . . . . . . . . . 13 (𝑥 = 𝑞 → (𝑥𝑔𝑢𝑞𝑔𝑢))
10 breq1 5033 . . . . . . . . . . . . 13 (𝑥 = 𝑞 → (𝑥𝑣𝑞𝑣))
119, 10anbi12d 633 . . . . . . . . . . . 12 (𝑥 = 𝑞 → ((𝑥𝑔𝑢𝑥𝑣) ↔ (𝑞𝑔𝑢𝑞𝑣)))
1211imbi1d 345 . . . . . . . . . . 11 (𝑥 = 𝑞 → (((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣) ↔ ((𝑞𝑔𝑢𝑞𝑣) → 𝑢 = 𝑣)))
1312imbi2d 344 . . . . . . . . . 10 (𝑥 = 𝑞 → (((𝜑 ∧ (𝑔𝐵𝐵)) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣)) ↔ ((𝜑 ∧ (𝑔𝐵𝐵)) → ((𝑞𝑔𝑢𝑞𝑣) → 𝑢 = 𝑣))))
14 frrlem11.3 . . . . . . . . . 10 ((𝜑 ∧ (𝑔𝐵𝐵)) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣))
1513, 14chvarvv 2005 . . . . . . . . 9 ((𝜑 ∧ (𝑔𝐵𝐵)) → ((𝑞𝑔𝑢𝑞𝑣) → 𝑢 = 𝑣))
167, 8, 15frrlem10 33245 . . . . . . . 8 ((𝜑𝑤 ∈ dom 𝐹) → (𝐹𝑤) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
175, 16sylan2 595 . . . . . . 7 ((𝜑𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹𝑤) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
1817adantlr 714 . . . . . 6 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹𝑤) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
19 frrlem11.4 . . . . . . . . 9 𝐶 = ((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})
2019fveq1i 6646 . . . . . . . 8 (𝐶𝑤) = (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑤)
216, 8, 14frrlem9 33244 . . . . . . . . . . . . 13 (𝜑 → Fun 𝐹)
22 funres 6366 . . . . . . . . . . . . 13 (Fun 𝐹 → Fun (𝐹𝑆))
2321, 22syl 17 . . . . . . . . . . . 12 (𝜑 → Fun (𝐹𝑆))
24 dmres 5840 . . . . . . . . . . . 12 dom (𝐹𝑆) = (𝑆 ∩ dom 𝐹)
25 df-fn 6327 . . . . . . . . . . . 12 ((𝐹𝑆) Fn (𝑆 ∩ dom 𝐹) ↔ (Fun (𝐹𝑆) ∧ dom (𝐹𝑆) = (𝑆 ∩ dom 𝐹)))
2623, 24, 25sylanblrc 593 . . . . . . . . . . 11 (𝜑 → (𝐹𝑆) Fn (𝑆 ∩ dom 𝐹))
2726adantr 484 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐹𝑆) Fn (𝑆 ∩ dom 𝐹))
2827adantr 484 . . . . . . . . 9 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹𝑆) Fn (𝑆 ∩ dom 𝐹))
29 vex 3444 . . . . . . . . . . 11 𝑧 ∈ V
30 ovex 7168 . . . . . . . . . . 11 (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))) ∈ V
3129, 30fnsn 6382 . . . . . . . . . 10 {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧}
3231a1i 11 . . . . . . . . 9 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧})
33 eldifn 4055 . . . . . . . . . . . . 13 (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ¬ 𝑧 ∈ dom 𝐹)
34 elinel2 4123 . . . . . . . . . . . . 13 (𝑧 ∈ (𝑆 ∩ dom 𝐹) → 𝑧 ∈ dom 𝐹)
3533, 34nsyl 142 . . . . . . . . . . . 12 (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ¬ 𝑧 ∈ (𝑆 ∩ dom 𝐹))
36 disjsn 4607 . . . . . . . . . . . 12 (((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ (𝑆 ∩ dom 𝐹))
3735, 36sylibr 237 . . . . . . . . . . 11 (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅)
3837adantl 485 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅)
3938adantr 484 . . . . . . . . 9 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → ((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅)
40 simpr 488 . . . . . . . . 9 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → 𝑤 ∈ (𝑆 ∩ dom 𝐹))
41 fvun1 6729 . . . . . . . . 9 (((𝐹𝑆) Fn (𝑆 ∩ dom 𝐹) ∧ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧} ∧ (((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅ ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹))) → (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑤) = ((𝐹𝑆)‘𝑤))
4228, 32, 39, 40, 41syl112anc 1371 . . . . . . . 8 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑤) = ((𝐹𝑆)‘𝑤))
4320, 42syl5eq 2845 . . . . . . 7 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶𝑤) = ((𝐹𝑆)‘𝑤))
44 elinel1 4122 . . . . . . . . 9 (𝑤 ∈ (𝑆 ∩ dom 𝐹) → 𝑤𝑆)
4544adantl 485 . . . . . . . 8 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → 𝑤𝑆)
4645fvresd 6665 . . . . . . 7 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → ((𝐹𝑆)‘𝑤) = (𝐹𝑤))
4743, 46eqtrd 2833 . . . . . 6 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶𝑤) = (𝐹𝑤))
486, 8, 14, 19frrlem11 33246 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))
49 fnfun 6423 . . . . . . . . . . 11 (𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → Fun 𝐶)
5048, 49syl 17 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → Fun 𝐶)
5150adantr 484 . . . . . . . . 9 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Fun 𝐶)
52 ssun1 4099 . . . . . . . . . . 11 (𝐹𝑆) ⊆ ((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})
5352, 19sseqtrri 3952 . . . . . . . . . 10 (𝐹𝑆) ⊆ 𝐶
5453a1i 11 . . . . . . . . 9 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹𝑆) ⊆ 𝐶)
55 eldifi 4054 . . . . . . . . . . . . 13 (𝑧 ∈ (𝐴 ∖ dom 𝐹) → 𝑧𝐴)
56 frrlem12.7 . . . . . . . . . . . . 13 ((𝜑𝑧𝐴) → ∀𝑤𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
5755, 56sylan2 595 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ∀𝑤𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
58 rspa 3171 . . . . . . . . . . . 12 ((∀𝑤𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆𝑤𝑆) → Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
5957, 44, 58syl2an 598 . . . . . . . . . . 11 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
606, 8frrlem8 33243 . . . . . . . . . . . . 13 (𝑤 ∈ dom 𝐹 → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹)
615, 60syl 17 . . . . . . . . . . . 12 (𝑤 ∈ (𝑆 ∩ dom 𝐹) → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹)
6261adantl 485 . . . . . . . . . . 11 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹)
6359, 62ssind 4159 . . . . . . . . . 10 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹))
6463, 24sseqtrrdi 3966 . . . . . . . . 9 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ dom (𝐹𝑆))
65 fun2ssres 6369 . . . . . . . . 9 ((Fun 𝐶 ∧ (𝐹𝑆) ⊆ 𝐶 ∧ Pred(𝑅, 𝐴, 𝑤) ⊆ dom (𝐹𝑆)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = ((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑤)))
6651, 54, 64, 65syl3anc 1368 . . . . . . . 8 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = ((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑤)))
6759resabs1d 5849 . . . . . . . 8 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → ((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑤)))
6866, 67eqtrd 2833 . . . . . . 7 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑤)))
6968oveq2d 7151 . . . . . 6 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
7018, 47, 693eqtr4d 2843 . . . . 5 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
7170ex 416 . . . 4 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑤 ∈ (𝑆 ∩ dom 𝐹) → (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
7229, 30fvsn 6920 . . . . . 6 ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧) = (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
7319fveq1i 6646 . . . . . . 7 (𝐶𝑧) = (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑧)
7431a1i 11 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧})
75 vsnid 4562 . . . . . . . . 9 𝑧 ∈ {𝑧}
7675a1i 11 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝑧 ∈ {𝑧})
77 fvun2 6730 . . . . . . . 8 (((𝐹𝑆) Fn (𝑆 ∩ dom 𝐹) ∧ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧} ∧ (((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅ ∧ 𝑧 ∈ {𝑧})) → (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑧) = ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧))
7827, 74, 38, 76, 77syl112anc 1371 . . . . . . 7 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑧) = ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧))
7973, 78syl5eq 2845 . . . . . 6 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐶𝑧) = ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧))
8019reseq1i 5814 . . . . . . . . 9 (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)) = (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ↾ Pred(𝑅, 𝐴, 𝑧))
81 resundir 5833 . . . . . . . . 9 (((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ↾ Pred(𝑅, 𝐴, 𝑧)) = (((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)))
8280, 81eqtri 2821 . . . . . . . 8 (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)) = (((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)))
83 frrlem12.6 . . . . . . . . . . . 12 ((𝜑𝑧𝐴) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
8455, 83sylan2 595 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
8584resabs1d 5849 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
86 frrlem12.5 . . . . . . . . . . . . 13 (𝜑𝑅 Fr 𝐴)
87 predfrirr 6145 . . . . . . . . . . . . 13 (𝑅 Fr 𝐴 → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧))
8886, 87syl 17 . . . . . . . . . . . 12 (𝜑 → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧))
8988adantr 484 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧))
90 ressnop0 6892 . . . . . . . . . . 11 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧) → ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)) = ∅)
9189, 90syl 17 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)) = ∅)
9285, 91uneq12d 4091 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧))) = ((𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ∅))
93 un0 4298 . . . . . . . . 9 ((𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ∅) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))
9492, 93eqtrdi 2849 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (((𝐹𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧))) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
9582, 94syl5eq 2845 . . . . . . 7 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
9695oveq2d 7151 . . . . . 6 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧))) = (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))))
9772, 79, 963eqtr4a 2859 . . . . 5 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐶𝑧) = (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧))))
98 fveq2 6645 . . . . . 6 (𝑤 = 𝑧 → (𝐶𝑤) = (𝐶𝑧))
99 id 22 . . . . . . 7 (𝑤 = 𝑧𝑤 = 𝑧)
100 predeq3 6120 . . . . . . . 8 (𝑤 = 𝑧 → Pred(𝑅, 𝐴, 𝑤) = Pred(𝑅, 𝐴, 𝑧))
101100reseq2d 5818 . . . . . . 7 (𝑤 = 𝑧 → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)))
10299, 101oveq12d 7153 . . . . . 6 (𝑤 = 𝑧 → (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))) = (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧))))
10398, 102eqeq12d 2814 . . . . 5 (𝑤 = 𝑧 → ((𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))) ↔ (𝐶𝑧) = (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)))))
10497, 103syl5ibrcom 250 . . . 4 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑤 = 𝑧 → (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
10571, 104jaod 856 . . 3 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ((𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 = 𝑧) → (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
1064, 105syl5bi 245 . 2 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
1071063impia 1114 1 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) → (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2111  {cab 2776  ∀wral 3106   ∖ cdif 3878   ∪ cun 3879   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243  {csn 4525  ⟨cop 4531   class class class wbr 5030   Fr wfr 5475  dom cdm 5519   ↾ cres 5521  Predcpred 6115  Fun wfun 6318   Fn wfn 6319  ‘cfv 6324  (class class class)co 7135  frecscfrecs 33230 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-id 5425  df-fr 5478  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-iota 6283  df-fun 6326  df-fn 6327  df-fv 6332  df-ov 7138  df-frecs 33231 This theorem is referenced by:  frrlem13  33248
 Copyright terms: Public domain W3C validator