Metamath Proof Explorer

Theorem wfrlem12

Description: Lemma for well-founded recursion. Here, we compute the value of the recursive definition generator. (Contributed by Scott Fenton, 21-Apr-2011) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Hypotheses wfrfun.1 ⊢ 𝑅 We 𝐴
wfrfun.2 ⊢ 𝑅 Se 𝐴
wfrfun.3 ⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 )
Assertion wfrlem12 ( 𝑦 ∈ dom 𝐹 → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 wfrfun.1 ⊢ 𝑅 We 𝐴
2 wfrfun.2 ⊢ 𝑅 Se 𝐴
3 wfrfun.3 ⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 )
4 vex ⊢ 𝑦 ∈ V
5 4 eldm2 ⊢ ( 𝑦 ∈ dom 𝐹 ↔ ∃ 𝑧 ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐹 )
6 df-wrecs ⊢ wrecs ( 𝑅 , 𝐴 , 𝐺 ) = ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
7 3 6 eqtri ⊢ 𝐹 = ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
8 7 eleq2i ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐹 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } )
9 eluniab ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ↔ ∃ 𝑓 ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ∧ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) )
10 8 9 bitri ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐹 ↔ ∃ 𝑓 ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ∧ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) )
11 abid ⊢ ( 𝑓 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ↔ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
12 elssuni ⊢ ( 𝑓 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } → 𝑓 ⊆ ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } )
13 12 7 sseqtrrdi ⊢ ( 𝑓 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } → 𝑓 ⊆ 𝐹 )
14 11 13 sylbir ⊢ ( ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) → 𝑓 ⊆ 𝐹 )
15 fnop ⊢ ( ( 𝑓 Fn 𝑥 ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ) → 𝑦 ∈ 𝑥 )
16 15 ex ⊢ ( 𝑓 Fn 𝑥 → ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 → 𝑦 ∈ 𝑥 ) )
17 rsp ⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) → ( 𝑦 ∈ 𝑥 → ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
18 17 impcom ⊢ ( ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) → ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )
19 rsp ⊢ ( ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 → ( 𝑦 ∈ 𝑥 → Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) )
20 fndm ⊢ ( 𝑓 Fn 𝑥 → dom 𝑓 = 𝑥 )
21 20 sseq2d ⊢ ( 𝑓 Fn 𝑥 → ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ dom 𝑓 ↔ Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) )
22 20 eleq2d ⊢ ( 𝑓 Fn 𝑥 → ( 𝑦 ∈ dom 𝑓 ↔ 𝑦 ∈ 𝑥 ) )
23 21 22 anbi12d ⊢ ( 𝑓 Fn 𝑥 → ( ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ dom 𝑓 ∧ 𝑦 ∈ dom 𝑓 ) ↔ ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑥 ) ) )
24 23 biimprd ⊢ ( 𝑓 Fn 𝑥 → ( ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑥 ) → ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ dom 𝑓 ∧ 𝑦 ∈ dom 𝑓 ) ) )
25 24 expd ⊢ ( 𝑓 Fn 𝑥 → ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 → ( 𝑦 ∈ 𝑥 → ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ dom 𝑓 ∧ 𝑦 ∈ dom 𝑓 ) ) ) )
26 25 impcom ⊢ ( ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ∧ 𝑓 Fn 𝑥 ) → ( 𝑦 ∈ 𝑥 → ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ dom 𝑓 ∧ 𝑦 ∈ dom 𝑓 ) ) )
27 1 2 3 wfrfun ⊢ Fun 𝐹
28 funssfv ⊢ ( ( Fun 𝐹 ∧ 𝑓 ⊆ 𝐹 ∧ 𝑦 ∈ dom 𝑓 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑓 ‘ 𝑦 ) )
29 28 3adant3l ⊢ ( ( Fun 𝐹 ∧ 𝑓 ⊆ 𝐹 ∧ ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ dom 𝑓 ∧ 𝑦 ∈ dom 𝑓 ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑓 ‘ 𝑦 ) )
30 fun2ssres ⊢ ( ( Fun 𝐹 ∧ 𝑓 ⊆ 𝐹 ∧ Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ dom 𝑓 ) → ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) )
31 30 3adant3r ⊢ ( ( Fun 𝐹 ∧ 𝑓 ⊆ 𝐹 ∧ ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ dom 𝑓 ∧ 𝑦 ∈ dom 𝑓 ) ) → ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) )
32 31 fveq2d ⊢ ( ( Fun 𝐹 ∧ 𝑓 ⊆ 𝐹 ∧ ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ dom 𝑓 ∧ 𝑦 ∈ dom 𝑓 ) ) → ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )
33 29 32 eqeq12d ⊢ ( ( Fun 𝐹 ∧ 𝑓 ⊆ 𝐹 ∧ ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ dom 𝑓 ∧ 𝑦 ∈ dom 𝑓 ) ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ↔ ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
34 33 biimprd ⊢ ( ( Fun 𝐹 ∧ 𝑓 ⊆ 𝐹 ∧ ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ dom 𝑓 ∧ 𝑦 ∈ dom 𝑓 ) ) → ( ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
35 27 34 mp3an1 ⊢ ( ( 𝑓 ⊆ 𝐹 ∧ ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ dom 𝑓 ∧ 𝑦 ∈ dom 𝑓 ) ) → ( ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
36 35 expcom ⊢ ( ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ dom 𝑓 ∧ 𝑦 ∈ dom 𝑓 ) → ( 𝑓 ⊆ 𝐹 → ( ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) )
37 36 com23 ⊢ ( ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ dom 𝑓 ∧ 𝑦 ∈ dom 𝑓 ) → ( ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) → ( 𝑓 ⊆ 𝐹 → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) )
38 26 37 syl6com ⊢ ( 𝑦 ∈ 𝑥 → ( ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ∧ 𝑓 Fn 𝑥 ) → ( ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) → ( 𝑓 ⊆ 𝐹 → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) ) )
39 38 expd ⊢ ( 𝑦 ∈ 𝑥 → ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 → ( 𝑓 Fn 𝑥 → ( ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) → ( 𝑓 ⊆ 𝐹 → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) ) ) )
40 39 com34 ⊢ ( 𝑦 ∈ 𝑥 → ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 → ( ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) → ( 𝑓 Fn 𝑥 → ( 𝑓 ⊆ 𝐹 → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) ) ) )
41 19 40 sylcom ⊢ ( ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 → ( 𝑦 ∈ 𝑥 → ( ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) → ( 𝑓 Fn 𝑥 → ( 𝑓 ⊆ 𝐹 → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) ) ) )
42 41 adantl ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) → ( 𝑦 ∈ 𝑥 → ( ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) → ( 𝑓 Fn 𝑥 → ( 𝑓 ⊆ 𝐹 → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) ) ) )
43 42 com14 ⊢ ( 𝑓 Fn 𝑥 → ( 𝑦 ∈ 𝑥 → ( ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) → ( ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) → ( 𝑓 ⊆ 𝐹 → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) ) ) )
44 18 43 syl7 ⊢ ( 𝑓 Fn 𝑥 → ( 𝑦 ∈ 𝑥 → ( ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) → ( ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) → ( 𝑓 ⊆ 𝐹 → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) ) ) )
45 44 exp4a ⊢ ( 𝑓 Fn 𝑥 → ( 𝑦 ∈ 𝑥 → ( 𝑦 ∈ 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) → ( ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) → ( 𝑓 ⊆ 𝐹 → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) ) ) ) )
46 45 pm2.43d ⊢ ( 𝑓 Fn 𝑥 → ( 𝑦 ∈ 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) → ( ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) → ( 𝑓 ⊆ 𝐹 → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) ) ) )
47 46 com34 ⊢ ( 𝑓 Fn 𝑥 → ( 𝑦 ∈ 𝑥 → ( ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) → ( 𝑓 ⊆ 𝐹 → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) ) ) )
48 16 47 syldc ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 → ( 𝑓 Fn 𝑥 → ( ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) → ( 𝑓 ⊆ 𝐹 → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) ) ) )
49 48 3impd ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 → ( ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) → ( 𝑓 ⊆ 𝐹 → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) )
50 49 exlimdv ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 → ( ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) → ( 𝑓 ⊆ 𝐹 → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) )
51 14 50 mpdi ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 → ( ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
52 51 imp ⊢ ( ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ∧ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )
53 52 exlimiv ⊢ ( ∃ 𝑓 ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑓 ∧ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )
54 10 53 sylbi ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐹 → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )
55 54 exlimiv ⊢ ( ∃ 𝑧 ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐹 → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )
56 5 55 sylbi ⊢ ( 𝑦 ∈ dom 𝐹 → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )