Metamath Proof Explorer

Theorem frrlem10

Description: Lemma for well-founded recursion. Under the compatibility hypothesis, compute the value of F within its domain. (Contributed by Scott Fenton, 6-Dec-2022)

Ref Expression
Hypotheses frrlem9.1 ⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
frrlem9.2 ⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
frrlem9.3 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ) → ( ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) → 𝑢 = 𝑣 ) )
Assertion frrlem10 ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 frrlem9.1 ⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
2 frrlem9.2 ⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
3 frrlem9.3 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ) → ( ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) → 𝑢 = 𝑣 ) )
4 vex ⊢ 𝑦 ∈ V
5 4 eldm2 ⊢ ( 𝑦 ∈ dom 𝐹 ↔ ∃ 𝑧 ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐹 )
6 1 2 frrlem5 ⊢ 𝐹 = ∪ 𝐵
7 1 unieqi ⊢ ∪ 𝐵 = ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
8 6 7 eqtri ⊢ 𝐹 = ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
9 8 eleq2i ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐹 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } )
10 eluniab ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ↔ ∃ 𝑓 ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ∧ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) )
11 9 10 bitri ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐹 ↔ ∃ 𝑓 ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ∧ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) )
12 19.8a ⊢ ( ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) → ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
13 12 3ad2ant2 ⊢ ( ( 𝜑 ∧ ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ) → ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
14 abid ⊢ ( 𝑓 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ↔ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
15 13 14 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ) → 𝑓 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } )
16 elssuni ⊢ ( 𝑓 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } → 𝑓 ⊆ ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } )
17 15 16 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ) → 𝑓 ⊆ ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } )
18 17 8 sseqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ) → 𝑓 ⊆ 𝐹 )
19 simpl23 ⊢ ( ( ( 𝜑 ∧ ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ) ∧ 𝑓 ⊆ 𝐹 ) → ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )
20 simpl3 ⊢ ( ( ( 𝜑 ∧ ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ) ∧ 𝑓 ⊆ 𝐹 ) → ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 )
21 vex ⊢ 𝑧 ∈ V
22 4 21 opeldm ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 → 𝑦 ∈ dom 𝑓 )
23 20 22 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ) ∧ 𝑓 ⊆ 𝐹 ) → 𝑦 ∈ dom 𝑓 )
24 simpl21 ⊢ ( ( ( 𝜑 ∧ ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ) ∧ 𝑓 ⊆ 𝐹 ) → 𝑓 Fn 𝑥 )
25 24 fndmd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ) ∧ 𝑓 ⊆ 𝐹 ) → dom 𝑓 = 𝑥 )
26 23 25 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ) ∧ 𝑓 ⊆ 𝐹 ) → 𝑦 ∈ 𝑥 )
27 rsp ⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) → ( 𝑦 ∈ 𝑥 → ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
28 19 26 27 sylc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ) ∧ 𝑓 ⊆ 𝐹 ) → ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )
29 simpl1 ⊢ ( ( ( 𝜑 ∧ ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ) ∧ 𝑓 ⊆ 𝐹 ) → 𝜑 )
30 1 2 3 frrlem9 ⊢ ( 𝜑 → Fun 𝐹 )
31 29 30 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ) ∧ 𝑓 ⊆ 𝐹 ) → Fun 𝐹 )
32 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ) ∧ 𝑓 ⊆ 𝐹 ) → 𝑓 ⊆ 𝐹 )
33 funssfv ⊢ ( ( Fun 𝐹 ∧ 𝑓 ⊆ 𝐹 ∧ 𝑦 ∈ dom 𝑓 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑓 ‘ 𝑦 ) )
34 31 32 23 33 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ) ∧ 𝑓 ⊆ 𝐹 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑓 ‘ 𝑦 ) )
35 simp22r ⊢ ( ( 𝜑 ∧ ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ) → ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 )
36 35 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ) ∧ 𝑓 ⊆ 𝐹 ) → ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 )
37 rsp ⊢ ( ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 → ( 𝑦 ∈ 𝑥 → Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) )
38 36 26 37 sylc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ) ∧ 𝑓 ⊆ 𝐹 ) → Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 )
39 38 25 sseqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ) ∧ 𝑓 ⊆ 𝐹 ) → Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ dom 𝑓 )
40 fun2ssres ⊢ ( ( Fun 𝐹 ∧ 𝑓 ⊆ 𝐹 ∧ Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ dom 𝑓 ) → ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) )
41 31 32 39 40 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ) ∧ 𝑓 ⊆ 𝐹 ) → ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) )
42 41 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ) ∧ 𝑓 ⊆ 𝐹 ) → ( 𝑦 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )
43 28 34 42 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ) ∧ 𝑓 ⊆ 𝐹 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )
44 18 43 mpdan ⊢ ( ( 𝜑 ∧ ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )
45 44 3exp ⊢ ( 𝜑 → ( ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) → ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) )
46 45 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) → ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) )
47 46 impcomd ⊢ ( 𝜑 → ( ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ∧ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
48 47 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑓 ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ∧ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
49 11 48 biimtrid ⊢ ( 𝜑 → ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐹 → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
50 49 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑧 ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐹 → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
51 5 50 biimtrid ⊢ ( 𝜑 → ( 𝑦 ∈ dom 𝐹 → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
52 51 imp ⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )