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 biimtrid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( 𝑤 ∈ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) → ( 𝐶 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) )
106 105 3impia ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ 𝑤 ∈ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ) → ( 𝐶 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) )