Metamath Proof Explorer

Theorem frrlem12

Description: Lemma for 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 funres ⊢ ( Fun 𝐹 → Fun ( 𝐹 ↾ 𝑆 ) )
26 24 25 syl ⊢ ( 𝜑 → Fun ( 𝐹 ↾ 𝑆 ) )
27 dmres ⊢ dom ( 𝐹 ↾ 𝑆 ) = ( 𝑆 ∩ dom 𝐹 )
28 df-fn ⊢ ( ( 𝐹 ↾ 𝑆 ) Fn ( 𝑆 ∩ dom 𝐹 ) ↔ ( Fun ( 𝐹 ↾ 𝑆 ) ∧ dom ( 𝐹 ↾ 𝑆 ) = ( 𝑆 ∩ dom 𝐹 ) ) )
29 26 27 28 sylanblrc ⊢ ( 𝜑 → ( 𝐹 ↾ 𝑆 ) Fn ( 𝑆 ∩ dom 𝐹 ) )
30 29 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( 𝐹 ↾ 𝑆 ) Fn ( 𝑆 ∩ dom 𝐹 ) )
31 30 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → ( 𝐹 ↾ 𝑆 ) Fn ( 𝑆 ∩ dom 𝐹 ) )
32 vex ⊢ 𝑧 ∈ V
33 ovex ⊢ ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ∈ V
34 32 33 fnsn ⊢ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } Fn { 𝑧 }
35 34 a1i ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } Fn { 𝑧 } )
36 eldifn ⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → ¬ 𝑧 ∈ dom 𝐹 )
37 elinel2 ⊢ ( 𝑧 ∈ ( 𝑆 ∩ dom 𝐹 ) → 𝑧 ∈ dom 𝐹 )
38 36 37 nsyl ⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → ¬ 𝑧 ∈ ( 𝑆 ∩ dom 𝐹 ) )
39 disjsn ⊢ ( ( ( 𝑆 ∩ dom 𝐹 ) ∩ { 𝑧 } ) = ∅ ↔ ¬ 𝑧 ∈ ( 𝑆 ∩ dom 𝐹 ) )
40 38 39 sylibr ⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → ( ( 𝑆 ∩ dom 𝐹 ) ∩ { 𝑧 } ) = ∅ )
41 40 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( ( 𝑆 ∩ dom 𝐹 ) ∩ { 𝑧 } ) = ∅ )
42 41 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → ( ( 𝑆 ∩ dom 𝐹 ) ∩ { 𝑧 } ) = ∅ )
43 simpr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) )
44 fvun1 ⊢ ( ( ( 𝐹 ↾ 𝑆 ) Fn ( 𝑆 ∩ dom 𝐹 ) ∧ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } Fn { 𝑧 } ∧ ( ( ( 𝑆 ∩ dom 𝐹 ) ∩ { 𝑧 } ) = ∅ ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) ) → ( ( ( 𝐹 ↾ 𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) ‘ 𝑤 ) = ( ( 𝐹 ↾ 𝑆 ) ‘ 𝑤 ) )
45 31 35 42 43 44 syl112anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → ( ( ( 𝐹 ↾ 𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) ‘ 𝑤 ) = ( ( 𝐹 ↾ 𝑆 ) ‘ 𝑤 ) )
46 23 45 syl5eq ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → ( 𝐶 ‘ 𝑤 ) = ( ( 𝐹 ↾ 𝑆 ) ‘ 𝑤 ) )
47 elinel1 ⊢ ( 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) → 𝑤 ∈ 𝑆 )
48 47 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → 𝑤 ∈ 𝑆 )
49 48 fvresd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → ( ( 𝐹 ↾ 𝑆 ) ‘ 𝑤 ) = ( 𝐹 ‘ 𝑤 ) )
50 46 49 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → ( 𝐶 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑤 ) )
51 1 2 3 4 frrlem11 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → 𝐶 Fn ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) )
52 fnfun ⊢ ( 𝐶 Fn ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) → Fun 𝐶 )
53 51 52 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → Fun 𝐶 )
54 53 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → Fun 𝐶 )
55 ssun1 ⊢ ( 𝐹 ↾ 𝑆 ) ⊆ ( ( 𝐹 ↾ 𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } )
56 55 4 sseqtrri ⊢ ( 𝐹 ↾ 𝑆 ) ⊆ 𝐶
57 56 a1i ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → ( 𝐹 ↾ 𝑆 ) ⊆ 𝐶 )
58 eldifi ⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → 𝑧 ∈ 𝐴 )
59 58 7 sylan2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ∀ 𝑤 ∈ 𝑆 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑆 )
60 rspa ⊢ ( ( ∀ 𝑤 ∈ 𝑆 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑆 ∧ 𝑤 ∈ 𝑆 ) → Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑆 )
61 59 47 60 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑆 )
62 1 2 frrlem8 ⊢ ( 𝑤 ∈ dom 𝐹 → Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ dom 𝐹 )
63 12 62 syl ⊢ ( 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) → Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ dom 𝐹 )
64 63 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ dom 𝐹 )
65 61 64 ssind ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ ( 𝑆 ∩ dom 𝐹 ) )
66 65 27 sseqtrrdi ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ dom ( 𝐹 ↾ 𝑆 ) )
67 fun2ssres ⊢ ( ( Fun 𝐶 ∧ ( 𝐹 ↾ 𝑆 ) ⊆ 𝐶 ∧ Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ dom ( 𝐹 ↾ 𝑆 ) ) → ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) = ( ( 𝐹 ↾ 𝑆 ) ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) )
68 54 57 66 67 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) = ( ( 𝐹 ↾ 𝑆 ) ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) )
69 61 resabs1d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → ( ( 𝐹 ↾ 𝑆 ) ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) = ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) )
70 68 69 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) = ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) )
71 70 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) = ( 𝑤 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) )
72 22 50 71 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ) → ( 𝐶 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) )
73 72 ex ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) → ( 𝐶 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) )
74 32 33 fvsn ⊢ ( { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) )
75 4 fveq1i ⊢ ( 𝐶 ‘ 𝑧 ) = ( ( ( 𝐹 ↾ 𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) ‘ 𝑧 )
76 34 a1i ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } Fn { 𝑧 } )
77 vsnid ⊢ 𝑧 ∈ { 𝑧 }
78 77 a1i ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → 𝑧 ∈ { 𝑧 } )
79 fvun2 ⊢ ( ( ( 𝐹 ↾ 𝑆 ) Fn ( 𝑆 ∩ dom 𝐹 ) ∧ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } Fn { 𝑧 } ∧ ( ( ( 𝑆 ∩ dom 𝐹 ) ∩ { 𝑧 } ) = ∅ ∧ 𝑧 ∈ { 𝑧 } ) ) → ( ( ( 𝐹 ↾ 𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) ‘ 𝑧 ) = ( { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ‘ 𝑧 ) )
80 30 76 41 78 79 syl112anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( ( ( 𝐹 ↾ 𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) ‘ 𝑧 ) = ( { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ‘ 𝑧 ) )
81 75 80 syl5eq ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( 𝐶 ‘ 𝑧 ) = ( { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ‘ 𝑧 ) )
82 4 reseq1i ⊢ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) = ( ( ( 𝐹 ↾ 𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) )
83 resundir ⊢ ( ( ( 𝐹 ↾ 𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) = ( ( ( 𝐹 ↾ 𝑆 ) ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ∪ ( { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) )
84 82 83 eqtri ⊢ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) = ( ( ( 𝐹 ↾ 𝑆 ) ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ∪ ( { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) )
85 58 6 sylan2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑆 )
86 85 resabs1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( ( 𝐹 ↾ 𝑆 ) ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) = ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) )
87 predfrirr ⊢ ( 𝑅 Fr 𝐴 → ¬ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) )
88 5 87 syl ⊢ ( 𝜑 → ¬ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) )
89 88 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ¬ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) )
90 ressnop0 ⊢ ( ¬ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) → ( { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) = ∅ )
91 89 90 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) = ∅ )
92 86 91 uneq12d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( ( ( 𝐹 ↾ 𝑆 ) ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ∪ ( { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) = ( ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ∪ ∅ ) )
93 un0 ⊢ ( ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ∪ ∅ ) = ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) )
94 92 93 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( ( ( 𝐹 ↾ 𝑆 ) ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ∪ ( { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) = ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) )
95 84 94 syl5eq ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) = ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) )
96 95 oveq2d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( 𝑧 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) = ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) )
97 74 81 96 3eqtr4a ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( 𝐶 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) )
98 fveq2 ⊢ ( 𝑤 = 𝑧 → ( 𝐶 ‘ 𝑤 ) = ( 𝐶 ‘ 𝑧 ) )
99 id ⊢ ( 𝑤 = 𝑧 → 𝑤 = 𝑧 )
100 predeq3 ⊢ ( 𝑤 = 𝑧 → Pred ( 𝑅 , 𝐴 , 𝑤 ) = Pred ( 𝑅 , 𝐴 , 𝑧 ) )
101 100 reseq2d ⊢ ( 𝑤 = 𝑧 → ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) = ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) )
102 99 101 oveq12d ⊢ ( 𝑤 = 𝑧 → ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) = ( 𝑧 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) )
103 98 102 eqeq12d ⊢ ( 𝑤 = 𝑧 → ( ( 𝐶 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ↔ ( 𝐶 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) )
104 97 103 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( 𝑤 = 𝑧 → ( 𝐶 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) )
105 73 104 jaod ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( ( 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ∨ 𝑤 = 𝑧 ) → ( 𝐶 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) )
106 11 105 syl5bi ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( 𝑤 ∈ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) → ( 𝐶 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) )
107 106 3impia ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ 𝑤 ∈ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ) → ( 𝐶 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) )