Metamath Proof Explorer


Theorem frrlem12

Description: Lemma for well-founded recursion. Next, we calculate the value of C . (Contributed by Scott Fenton, 7-Dec-2022)

Ref Expression
Hypotheses frrlem11.1 𝐵 = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥𝐴 ∧ ∀ 𝑦𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
frrlem11.2 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
frrlem11.3 ( ( 𝜑 ∧ ( 𝑔𝐵𝐵 ) ) → ( ( 𝑥 𝑔 𝑢𝑥 𝑣 ) → 𝑢 = 𝑣 ) )
frrlem11.4 𝐶 = ( ( 𝐹𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } )
frrlem12.5 ( 𝜑𝑅 Fr 𝐴 )
frrlem12.6 ( ( 𝜑𝑧𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑆 )
frrlem12.7 ( ( 𝜑𝑧𝐴 ) → ∀ 𝑤𝑆 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑆 )
Assertion frrlem12 ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ 𝑤 ∈ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ) → ( 𝐶𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) )

Proof

Step Hyp Ref Expression
1 frrlem11.1 𝐵 = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥𝐴 ∧ ∀ 𝑦𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
2 frrlem11.2 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
3 frrlem11.3 ( ( 𝜑 ∧ ( 𝑔𝐵𝐵 ) ) → ( ( 𝑥 𝑔 𝑢𝑥 𝑣 ) → 𝑢 = 𝑣 ) )
4 frrlem11.4 𝐶 = ( ( 𝐹𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } )
5 frrlem12.5 ( 𝜑𝑅 Fr 𝐴 )
6 frrlem12.6 ( ( 𝜑𝑧𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑆 )
7 frrlem12.7 ( ( 𝜑𝑧𝐴 ) → ∀ 𝑤𝑆 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑆 )
8 elun ( 𝑤 ∈ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ↔ ( 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ∨ 𝑤 ∈ { 𝑧 } ) )
9 velsn ( 𝑤 ∈ { 𝑧 } ↔ 𝑤 = 𝑧 )
10 9 orbi2i ( ( 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ∨ 𝑤 ∈ { 𝑧 } ) ↔ ( 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ∨ 𝑤 = 𝑧 ) )
11 8 10 bitri ( 𝑤 ∈ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ↔ ( 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ∨ 𝑤 = 𝑧 ) )
12 elinel2 ( 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) → 𝑤 ∈ dom 𝐹 )
13 1 frrlem1 𝐵 = { 𝑝 ∣ ∃ 𝑞 ( 𝑝 Fn 𝑞 ∧ ( 𝑞𝐴 ∧ ∀ 𝑤𝑞 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑞 ) ∧ ∀ 𝑤𝑞 ( 𝑝𝑤 ) = ( 𝑤 𝐺 ( 𝑝 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) }
14 breq1 ( 𝑥 = 𝑞 → ( 𝑥 𝑔 𝑢𝑞 𝑔 𝑢 ) )
15 breq1 ( 𝑥 = 𝑞 → ( 𝑥 𝑣𝑞 𝑣 ) )
16 14 15 anbi12d ( 𝑥 = 𝑞 → ( ( 𝑥 𝑔 𝑢𝑥 𝑣 ) ↔ ( 𝑞 𝑔 𝑢𝑞 𝑣 ) ) )
17 16 imbi1d ( 𝑥 = 𝑞 → ( ( ( 𝑥 𝑔 𝑢𝑥 𝑣 ) → 𝑢 = 𝑣 ) ↔ ( ( 𝑞 𝑔 𝑢𝑞 𝑣 ) → 𝑢 = 𝑣 ) ) )
18 17 imbi2d ( 𝑥 = 𝑞 → ( ( ( 𝜑 ∧ ( 𝑔𝐵𝐵 ) ) → ( ( 𝑥 𝑔 𝑢𝑥 𝑣 ) → 𝑢 = 𝑣 ) ) ↔ ( ( 𝜑 ∧ ( 𝑔𝐵𝐵 ) ) → ( ( 𝑞 𝑔 𝑢𝑞 𝑣 ) → 𝑢 = 𝑣 ) ) ) )
19 18 3 chvarvv ( ( 𝜑 ∧ ( 𝑔𝐵𝐵 ) ) → ( ( 𝑞 𝑔 𝑢𝑞 𝑣 ) → 𝑢 = 𝑣 ) )
20 13 2 19 frrlem10 ( ( 𝜑𝑤 ∈ dom 𝐹 ) → ( 𝐹𝑤 ) = ( 𝑤 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) )
21 12 20 sylan2 ( ( 𝜑𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → ( 𝐹𝑤 ) = ( 𝑤 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) )
22 21 adantlr ( ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → ( 𝐹𝑤 ) = ( 𝑤 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) )
23 4 fveq1i ( 𝐶𝑤 ) = ( ( ( 𝐹𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) ‘ 𝑤 )
24 1 2 3 frrlem9 ( 𝜑 → Fun 𝐹 )
25 24 funresd ( 𝜑 → Fun ( 𝐹𝑆 ) )
26 dmres dom ( 𝐹𝑆 ) = ( 𝑆 ∩ dom 𝐹 )
27 df-fn ( ( 𝐹𝑆 ) Fn ( 𝑆 ∩ dom 𝐹 ) ↔ ( Fun ( 𝐹𝑆 ) ∧ dom ( 𝐹𝑆 ) = ( 𝑆 ∩ dom 𝐹 ) ) )
28 25 26 27 sylanblrc ( 𝜑 → ( 𝐹𝑆 ) Fn ( 𝑆 ∩ dom 𝐹 ) )
29 28 adantr ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( 𝐹𝑆 ) Fn ( 𝑆 ∩ dom 𝐹 ) )
30 29 adantr ( ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → ( 𝐹𝑆 ) Fn ( 𝑆 ∩ dom 𝐹 ) )
31 vex 𝑧 ∈ V
32 ovex ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ∈ V
33 31 32 fnsn { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } Fn { 𝑧 }
34 33 a1i ( ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } Fn { 𝑧 } )
35 eldifn ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → ¬ 𝑧 ∈ dom 𝐹 )
36 elinel2 ( 𝑧 ∈ ( 𝑆 ∩ dom 𝐹 ) → 𝑧 ∈ dom 𝐹 )
37 35 36 nsyl ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → ¬ 𝑧 ∈ ( 𝑆 ∩ dom 𝐹 ) )
38 disjsn ( ( ( 𝑆 ∩ dom 𝐹 ) ∩ { 𝑧 } ) = ∅ ↔ ¬ 𝑧 ∈ ( 𝑆 ∩ dom 𝐹 ) )
39 37 38 sylibr ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → ( ( 𝑆 ∩ dom 𝐹 ) ∩ { 𝑧 } ) = ∅ )
40 39 adantl ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( ( 𝑆 ∩ dom 𝐹 ) ∩ { 𝑧 } ) = ∅ )
41 40 adantr ( ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → ( ( 𝑆 ∩ dom 𝐹 ) ∩ { 𝑧 } ) = ∅ )
42 simpr ( ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) )
43 fvun1 ( ( ( 𝐹𝑆 ) Fn ( 𝑆 ∩ dom 𝐹 ) ∧ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } Fn { 𝑧 } ∧ ( ( ( 𝑆 ∩ dom 𝐹 ) ∩ { 𝑧 } ) = ∅ ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) ) → ( ( ( 𝐹𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) ‘ 𝑤 ) = ( ( 𝐹𝑆 ) ‘ 𝑤 ) )
44 30 34 41 42 43 syl112anc ( ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → ( ( ( 𝐹𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) ‘ 𝑤 ) = ( ( 𝐹𝑆 ) ‘ 𝑤 ) )
45 23 44 eqtrid ( ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → ( 𝐶𝑤 ) = ( ( 𝐹𝑆 ) ‘ 𝑤 ) )
46 elinel1 ( 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) → 𝑤𝑆 )
47 46 adantl ( ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → 𝑤𝑆 )
48 47 fvresd ( ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → ( ( 𝐹𝑆 ) ‘ 𝑤 ) = ( 𝐹𝑤 ) )
49 45 48 eqtrd ( ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → ( 𝐶𝑤 ) = ( 𝐹𝑤 ) )
50 1 2 3 4 frrlem11 ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → 𝐶 Fn ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) )
51 fnfun ( 𝐶 Fn ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) → Fun 𝐶 )
52 50 51 syl ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → Fun 𝐶 )
53 52 adantr ( ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → Fun 𝐶 )
54 ssun1 ( 𝐹𝑆 ) ⊆ ( ( 𝐹𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } )
55 54 4 sseqtrri ( 𝐹𝑆 ) ⊆ 𝐶
56 55 a1i ( ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → ( 𝐹𝑆 ) ⊆ 𝐶 )
57 eldifi ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → 𝑧𝐴 )
58 57 7 sylan2 ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ∀ 𝑤𝑆 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑆 )
59 rspa ( ( ∀ 𝑤𝑆 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑆𝑤𝑆 ) → Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑆 )
60 58 46 59 syl2an ( ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑆 )
61 1 2 frrlem8 ( 𝑤 ∈ dom 𝐹 → Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ dom 𝐹 )
62 12 61 syl ( 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) → Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ dom 𝐹 )
63 62 adantl ( ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ dom 𝐹 )
64 60 63 ssind ( ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ ( 𝑆 ∩ dom 𝐹 ) )
65 64 26 sseqtrrdi ( ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ dom ( 𝐹𝑆 ) )
66 fun2ssres ( ( Fun 𝐶 ∧ ( 𝐹𝑆 ) ⊆ 𝐶 ∧ Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ dom ( 𝐹𝑆 ) ) → ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) = ( ( 𝐹𝑆 ) ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) )
67 53 56 65 66 syl3anc ( ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) = ( ( 𝐹𝑆 ) ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) )
68 60 resabs1d ( ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → ( ( 𝐹𝑆 ) ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) = ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) )
69 67 68 eqtrd ( ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) = ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) )
70 69 oveq2d ( ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) = ( 𝑤 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) )
71 22 49 70 3eqtr4d ( ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → ( 𝐶𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) )
72 71 ex ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) → ( 𝐶𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) )
73 31 32 fvsn ( { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) )
74 4 fveq1i ( 𝐶𝑧 ) = ( ( ( 𝐹𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) ‘ 𝑧 )
75 33 a1i ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } Fn { 𝑧 } )
76 vsnid 𝑧 ∈ { 𝑧 }
77 76 a1i ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → 𝑧 ∈ { 𝑧 } )
78 fvun2 ( ( ( 𝐹𝑆 ) Fn ( 𝑆 ∩ dom 𝐹 ) ∧ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } Fn { 𝑧 } ∧ ( ( ( 𝑆 ∩ dom 𝐹 ) ∩ { 𝑧 } ) = ∅ ∧ 𝑧 ∈ { 𝑧 } ) ) → ( ( ( 𝐹𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) ‘ 𝑧 ) = ( { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ‘ 𝑧 ) )
79 29 75 40 77 78 syl112anc ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( ( ( 𝐹𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) ‘ 𝑧 ) = ( { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ‘ 𝑧 ) )
80 74 79 eqtrid ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( 𝐶𝑧 ) = ( { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ‘ 𝑧 ) )
81 4 reseq1i ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) = ( ( ( 𝐹𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) )
82 resundir ( ( ( 𝐹𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) = ( ( ( 𝐹𝑆 ) ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ∪ ( { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) )
83 81 82 eqtri ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) = ( ( ( 𝐹𝑆 ) ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ∪ ( { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) )
84 57 6 sylan2 ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑆 )
85 84 resabs1d ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( ( 𝐹𝑆 ) ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) = ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) )
86 predfrirr ( 𝑅 Fr 𝐴 → ¬ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) )
87 5 86 syl ( 𝜑 → ¬ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) )
88 87 adantr ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ¬ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) )
89 ressnop0 ( ¬ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) → ( { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) = ∅ )
90 88 89 syl ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) = ∅ )
91 85 90 uneq12d ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( ( ( 𝐹𝑆 ) ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ∪ ( { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) = ( ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ∪ ∅ ) )
92 un0 ( ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ∪ ∅ ) = ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) )
93 91 92 eqtrdi ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( ( ( 𝐹𝑆 ) ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ∪ ( { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) = ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) )
94 83 93 eqtrid ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) = ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) )
95 94 oveq2d ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( 𝑧 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) = ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) )
96 73 80 95 3eqtr4a ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( 𝐶𝑧 ) = ( 𝑧 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) )
97 fveq2 ( 𝑤 = 𝑧 → ( 𝐶𝑤 ) = ( 𝐶𝑧 ) )
98 id ( 𝑤 = 𝑧𝑤 = 𝑧 )
99 predeq3 ( 𝑤 = 𝑧 → Pred ( 𝑅 , 𝐴 , 𝑤 ) = Pred ( 𝑅 , 𝐴 , 𝑧 ) )
100 99 reseq2d ( 𝑤 = 𝑧 → ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) = ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) )
101 98 100 oveq12d ( 𝑤 = 𝑧 → ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) = ( 𝑧 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) )
102 97 101 eqeq12d ( 𝑤 = 𝑧 → ( ( 𝐶𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ↔ ( 𝐶𝑧 ) = ( 𝑧 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) )
103 96 102 syl5ibrcom ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( 𝑤 = 𝑧 → ( 𝐶𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) )
104 72 103 jaod ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( ( 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ∨ 𝑤 = 𝑧 ) → ( 𝐶𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) )
105 11 104 syl5bi ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( 𝑤 ∈ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) → ( 𝐶𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) )
106 105 3impia ( ( 𝜑𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ 𝑤 ∈ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ) → ( 𝐶𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) )