Metamath Proof Explorer


Theorem frrlem4

Description: Lemma for well-founded recursion. Properties of the restriction of an acceptable function to the domain of another acceptable function. (Contributed by Paul Chapman, 21-Apr-2012)

Ref Expression
Hypothesis frrlem4.1 𝐵 = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥𝐴 ∧ ∀ 𝑦𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
Assertion frrlem4 ( ( 𝑔𝐵𝐵 ) → ( ( 𝑔 ↾ ( dom 𝑔 ∩ dom ) ) Fn ( dom 𝑔 ∩ dom ) ∧ ∀ 𝑎 ∈ ( dom 𝑔 ∩ dom ) ( ( 𝑔 ↾ ( dom 𝑔 ∩ dom ) ) ‘ 𝑎 ) = ( 𝑎 𝐺 ( ( 𝑔 ↾ ( dom 𝑔 ∩ dom ) ) ↾ Pred ( 𝑅 , ( dom 𝑔 ∩ dom ) , 𝑎 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 frrlem4.1 𝐵 = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥𝐴 ∧ ∀ 𝑦𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
2 1 frrlem2 ( 𝑔𝐵 → Fun 𝑔 )
3 2 funfnd ( 𝑔𝐵𝑔 Fn dom 𝑔 )
4 fnresin1 ( 𝑔 Fn dom 𝑔 → ( 𝑔 ↾ ( dom 𝑔 ∩ dom ) ) Fn ( dom 𝑔 ∩ dom ) )
5 3 4 syl ( 𝑔𝐵 → ( 𝑔 ↾ ( dom 𝑔 ∩ dom ) ) Fn ( dom 𝑔 ∩ dom ) )
6 5 adantr ( ( 𝑔𝐵𝐵 ) → ( 𝑔 ↾ ( dom 𝑔 ∩ dom ) ) Fn ( dom 𝑔 ∩ dom ) )
7 1 frrlem1 𝐵 = { 𝑔 ∣ ∃ 𝑏 ( 𝑔 Fn 𝑏 ∧ ( 𝑏𝐴 ∧ ∀ 𝑎𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ∀ 𝑎𝑏 ( 𝑔𝑎 ) = ( 𝑎 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) }
8 7 abeq2i ( 𝑔𝐵 ↔ ∃ 𝑏 ( 𝑔 Fn 𝑏 ∧ ( 𝑏𝐴 ∧ ∀ 𝑎𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ∀ 𝑎𝑏 ( 𝑔𝑎 ) = ( 𝑎 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) )
9 fndm ( 𝑔 Fn 𝑏 → dom 𝑔 = 𝑏 )
10 9 adantr ( ( 𝑔 Fn 𝑏 ∧ ( 𝑏𝐴 ∧ ∀ 𝑎𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ) → dom 𝑔 = 𝑏 )
11 10 raleqdv ( ( 𝑔 Fn 𝑏 ∧ ( 𝑏𝐴 ∧ ∀ 𝑎𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ) → ( ∀ 𝑎 ∈ dom 𝑔 ( 𝑔𝑎 ) = ( 𝑎 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ↔ ∀ 𝑎𝑏 ( 𝑔𝑎 ) = ( 𝑎 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) )
12 11 biimp3ar ( ( 𝑔 Fn 𝑏 ∧ ( 𝑏𝐴 ∧ ∀ 𝑎𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ∀ 𝑎𝑏 ( 𝑔𝑎 ) = ( 𝑎 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) → ∀ 𝑎 ∈ dom 𝑔 ( 𝑔𝑎 ) = ( 𝑎 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) )
13 rsp ( ∀ 𝑎 ∈ dom 𝑔 ( 𝑔𝑎 ) = ( 𝑎 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) → ( 𝑎 ∈ dom 𝑔 → ( 𝑔𝑎 ) = ( 𝑎 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) )
14 12 13 syl ( ( 𝑔 Fn 𝑏 ∧ ( 𝑏𝐴 ∧ ∀ 𝑎𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ∀ 𝑎𝑏 ( 𝑔𝑎 ) = ( 𝑎 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) → ( 𝑎 ∈ dom 𝑔 → ( 𝑔𝑎 ) = ( 𝑎 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) )
15 14 exlimiv ( ∃ 𝑏 ( 𝑔 Fn 𝑏 ∧ ( 𝑏𝐴 ∧ ∀ 𝑎𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ∀ 𝑎𝑏 ( 𝑔𝑎 ) = ( 𝑎 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) → ( 𝑎 ∈ dom 𝑔 → ( 𝑔𝑎 ) = ( 𝑎 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) )
16 8 15 sylbi ( 𝑔𝐵 → ( 𝑎 ∈ dom 𝑔 → ( 𝑔𝑎 ) = ( 𝑎 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) )
17 elinel1 ( 𝑎 ∈ ( dom 𝑔 ∩ dom ) → 𝑎 ∈ dom 𝑔 )
18 16 17 impel ( ( 𝑔𝐵𝑎 ∈ ( dom 𝑔 ∩ dom ) ) → ( 𝑔𝑎 ) = ( 𝑎 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) )
19 18 adantlr ( ( ( 𝑔𝐵𝐵 ) ∧ 𝑎 ∈ ( dom 𝑔 ∩ dom ) ) → ( 𝑔𝑎 ) = ( 𝑎 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) )
20 simpr ( ( ( 𝑔𝐵𝐵 ) ∧ 𝑎 ∈ ( dom 𝑔 ∩ dom ) ) → 𝑎 ∈ ( dom 𝑔 ∩ dom ) )
21 20 fvresd ( ( ( 𝑔𝐵𝐵 ) ∧ 𝑎 ∈ ( dom 𝑔 ∩ dom ) ) → ( ( 𝑔 ↾ ( dom 𝑔 ∩ dom ) ) ‘ 𝑎 ) = ( 𝑔𝑎 ) )
22 resres ( ( 𝑔 ↾ ( dom 𝑔 ∩ dom ) ) ↾ Pred ( 𝑅 , ( dom 𝑔 ∩ dom ) , 𝑎 ) ) = ( 𝑔 ↾ ( ( dom 𝑔 ∩ dom ) ∩ Pred ( 𝑅 , ( dom 𝑔 ∩ dom ) , 𝑎 ) ) )
23 predss Pred ( 𝑅 , ( dom 𝑔 ∩ dom ) , 𝑎 ) ⊆ ( dom 𝑔 ∩ dom )
24 sseqin2 ( Pred ( 𝑅 , ( dom 𝑔 ∩ dom ) , 𝑎 ) ⊆ ( dom 𝑔 ∩ dom ) ↔ ( ( dom 𝑔 ∩ dom ) ∩ Pred ( 𝑅 , ( dom 𝑔 ∩ dom ) , 𝑎 ) ) = Pred ( 𝑅 , ( dom 𝑔 ∩ dom ) , 𝑎 ) )
25 23 24 mpbi ( ( dom 𝑔 ∩ dom ) ∩ Pred ( 𝑅 , ( dom 𝑔 ∩ dom ) , 𝑎 ) ) = Pred ( 𝑅 , ( dom 𝑔 ∩ dom ) , 𝑎 )
26 1 frrlem1 𝐵 = { ∣ ∃ 𝑐 ( Fn 𝑐 ∧ ( 𝑐𝐴 ∧ ∀ 𝑎𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ∧ ∀ 𝑎𝑐 ( 𝑎 ) = ( 𝑎 𝐺 ( ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) }
27 26 abeq2i ( 𝐵 ↔ ∃ 𝑐 ( Fn 𝑐 ∧ ( 𝑐𝐴 ∧ ∀ 𝑎𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ∧ ∀ 𝑎𝑐 ( 𝑎 ) = ( 𝑎 𝐺 ( ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) )
28 exdistrv ( ∃ 𝑏𝑐 ( ( 𝑔 Fn 𝑏 ∧ ( 𝑏𝐴 ∧ ∀ 𝑎𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ∀ 𝑎𝑏 ( 𝑔𝑎 ) = ( 𝑎 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ∧ ( Fn 𝑐 ∧ ( 𝑐𝐴 ∧ ∀ 𝑎𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ∧ ∀ 𝑎𝑐 ( 𝑎 ) = ( 𝑎 𝐺 ( ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ) ↔ ( ∃ 𝑏 ( 𝑔 Fn 𝑏 ∧ ( 𝑏𝐴 ∧ ∀ 𝑎𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ∀ 𝑎𝑏 ( 𝑔𝑎 ) = ( 𝑎 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ∧ ∃ 𝑐 ( Fn 𝑐 ∧ ( 𝑐𝐴 ∧ ∀ 𝑎𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ∧ ∀ 𝑎𝑐 ( 𝑎 ) = ( 𝑎 𝐺 ( ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ) )
29 inss1 ( 𝑏𝑐 ) ⊆ 𝑏
30 simpl2l ( ( ( 𝑔 Fn 𝑏 ∧ ( 𝑏𝐴 ∧ ∀ 𝑎𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ∀ 𝑎𝑏 ( 𝑔𝑎 ) = ( 𝑎 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ∧ ( Fn 𝑐 ∧ ( 𝑐𝐴 ∧ ∀ 𝑎𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ∧ ∀ 𝑎𝑐 ( 𝑎 ) = ( 𝑎 𝐺 ( ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ) → 𝑏𝐴 )
31 29 30 sstrid ( ( ( 𝑔 Fn 𝑏 ∧ ( 𝑏𝐴 ∧ ∀ 𝑎𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ∀ 𝑎𝑏 ( 𝑔𝑎 ) = ( 𝑎 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ∧ ( Fn 𝑐 ∧ ( 𝑐𝐴 ∧ ∀ 𝑎𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ∧ ∀ 𝑎𝑐 ( 𝑎 ) = ( 𝑎 𝐺 ( ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ) → ( 𝑏𝑐 ) ⊆ 𝐴 )
32 simp2r ( ( 𝑔 Fn 𝑏 ∧ ( 𝑏𝐴 ∧ ∀ 𝑎𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ∀ 𝑎𝑏 ( 𝑔𝑎 ) = ( 𝑎 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) → ∀ 𝑎𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 )
33 simp2r ( ( Fn 𝑐 ∧ ( 𝑐𝐴 ∧ ∀ 𝑎𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ∧ ∀ 𝑎𝑐 ( 𝑎 ) = ( 𝑎 𝐺 ( ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) → ∀ 𝑎𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 )
34 nfra1 𝑎𝑎𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏
35 nfra1 𝑎𝑎𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐
36 34 35 nfan 𝑎 ( ∀ 𝑎𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ∧ ∀ 𝑎𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 )
37 elinel1 ( 𝑎 ∈ ( 𝑏𝑐 ) → 𝑎𝑏 )
38 rsp ( ∀ 𝑎𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 → ( 𝑎𝑏 → Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) )
39 37 38 syl5com ( 𝑎 ∈ ( 𝑏𝑐 ) → ( ∀ 𝑎𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 → Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) )
40 elinel2 ( 𝑎 ∈ ( 𝑏𝑐 ) → 𝑎𝑐 )
41 rsp ( ∀ 𝑎𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 → ( 𝑎𝑐 → Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) )
42 40 41 syl5com ( 𝑎 ∈ ( 𝑏𝑐 ) → ( ∀ 𝑎𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 → Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) )
43 39 42 anim12d ( 𝑎 ∈ ( 𝑏𝑐 ) → ( ( ∀ 𝑎𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ∧ ∀ 𝑎𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) → ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ∧ Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ) )
44 ssin ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ∧ Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ↔ Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( 𝑏𝑐 ) )
45 44 biimpi ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ∧ Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) → Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( 𝑏𝑐 ) )
46 43 45 syl6com ( ( ∀ 𝑎𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ∧ ∀ 𝑎𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) → ( 𝑎 ∈ ( 𝑏𝑐 ) → Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( 𝑏𝑐 ) ) )
47 36 46 ralrimi ( ( ∀ 𝑎𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ∧ ∀ 𝑎𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) → ∀ 𝑎 ∈ ( 𝑏𝑐 ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( 𝑏𝑐 ) )
48 32 33 47 syl2an ( ( ( 𝑔 Fn 𝑏 ∧ ( 𝑏𝐴 ∧ ∀ 𝑎𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ∀ 𝑎𝑏 ( 𝑔𝑎 ) = ( 𝑎 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ∧ ( Fn 𝑐 ∧ ( 𝑐𝐴 ∧ ∀ 𝑎𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ∧ ∀ 𝑎𝑐 ( 𝑎 ) = ( 𝑎 𝐺 ( ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ) → ∀ 𝑎 ∈ ( 𝑏𝑐 ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( 𝑏𝑐 ) )
49 simpl1 ( ( ( 𝑔 Fn 𝑏 ∧ ( 𝑏𝐴 ∧ ∀ 𝑎𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ∀ 𝑎𝑏 ( 𝑔𝑎 ) = ( 𝑎 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ∧ ( Fn 𝑐 ∧ ( 𝑐𝐴 ∧ ∀ 𝑎𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ∧ ∀ 𝑎𝑐 ( 𝑎 ) = ( 𝑎 𝐺 ( ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ) → 𝑔 Fn 𝑏 )
50 49 fndmd ( ( ( 𝑔 Fn 𝑏 ∧ ( 𝑏𝐴 ∧ ∀ 𝑎𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ∀ 𝑎𝑏 ( 𝑔𝑎 ) = ( 𝑎 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ∧ ( Fn 𝑐 ∧ ( 𝑐𝐴 ∧ ∀ 𝑎𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ∧ ∀ 𝑎𝑐 ( 𝑎 ) = ( 𝑎 𝐺 ( ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ) → dom 𝑔 = 𝑏 )
51 simpr1 ( ( ( 𝑔 Fn 𝑏 ∧ ( 𝑏𝐴 ∧ ∀ 𝑎𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ∀ 𝑎𝑏 ( 𝑔𝑎 ) = ( 𝑎 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ∧ ( Fn 𝑐 ∧ ( 𝑐𝐴 ∧ ∀ 𝑎𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ∧ ∀ 𝑎𝑐 ( 𝑎 ) = ( 𝑎 𝐺 ( ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ) → Fn 𝑐 )
52 51 fndmd ( ( ( 𝑔 Fn 𝑏 ∧ ( 𝑏𝐴 ∧ ∀ 𝑎𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ∀ 𝑎𝑏 ( 𝑔𝑎 ) = ( 𝑎 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ∧ ( Fn 𝑐 ∧ ( 𝑐𝐴 ∧ ∀ 𝑎𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ∧ ∀ 𝑎𝑐 ( 𝑎 ) = ( 𝑎 𝐺 ( ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ) → dom = 𝑐 )
53 ineq12 ( ( dom 𝑔 = 𝑏 ∧ dom = 𝑐 ) → ( dom 𝑔 ∩ dom ) = ( 𝑏𝑐 ) )
54 53 sseq1d ( ( dom 𝑔 = 𝑏 ∧ dom = 𝑐 ) → ( ( dom 𝑔 ∩ dom ) ⊆ 𝐴 ↔ ( 𝑏𝑐 ) ⊆ 𝐴 ) )
55 53 sseq2d ( ( dom 𝑔 = 𝑏 ∧ dom = 𝑐 ) → ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( dom 𝑔 ∩ dom ) ↔ Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( 𝑏𝑐 ) ) )
56 53 55 raleqbidv ( ( dom 𝑔 = 𝑏 ∧ dom = 𝑐 ) → ( ∀ 𝑎 ∈ ( dom 𝑔 ∩ dom ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( dom 𝑔 ∩ dom ) ↔ ∀ 𝑎 ∈ ( 𝑏𝑐 ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( 𝑏𝑐 ) ) )
57 54 56 anbi12d ( ( dom 𝑔 = 𝑏 ∧ dom = 𝑐 ) → ( ( ( dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀ 𝑎 ∈ ( dom 𝑔 ∩ dom ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( dom 𝑔 ∩ dom ) ) ↔ ( ( 𝑏𝑐 ) ⊆ 𝐴 ∧ ∀ 𝑎 ∈ ( 𝑏𝑐 ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( 𝑏𝑐 ) ) ) )
58 50 52 57 syl2anc ( ( ( 𝑔 Fn 𝑏 ∧ ( 𝑏𝐴 ∧ ∀ 𝑎𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ∀ 𝑎𝑏 ( 𝑔𝑎 ) = ( 𝑎 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ∧ ( Fn 𝑐 ∧ ( 𝑐𝐴 ∧ ∀ 𝑎𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ∧ ∀ 𝑎𝑐 ( 𝑎 ) = ( 𝑎 𝐺 ( ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ) → ( ( ( dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀ 𝑎 ∈ ( dom 𝑔 ∩ dom ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( dom 𝑔 ∩ dom ) ) ↔ ( ( 𝑏𝑐 ) ⊆ 𝐴 ∧ ∀ 𝑎 ∈ ( 𝑏𝑐 ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( 𝑏𝑐 ) ) ) )
59 31 48 58 mpbir2and ( ( ( 𝑔 Fn 𝑏 ∧ ( 𝑏𝐴 ∧ ∀ 𝑎𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ∀ 𝑎𝑏 ( 𝑔𝑎 ) = ( 𝑎 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ∧ ( Fn 𝑐 ∧ ( 𝑐𝐴 ∧ ∀ 𝑎𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ∧ ∀ 𝑎𝑐 ( 𝑎 ) = ( 𝑎 𝐺 ( ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ) → ( ( dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀ 𝑎 ∈ ( dom 𝑔 ∩ dom ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( dom 𝑔 ∩ dom ) ) )
60 59 exlimivv ( ∃ 𝑏𝑐 ( ( 𝑔 Fn 𝑏 ∧ ( 𝑏𝐴 ∧ ∀ 𝑎𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ∀ 𝑎𝑏 ( 𝑔𝑎 ) = ( 𝑎 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ∧ ( Fn 𝑐 ∧ ( 𝑐𝐴 ∧ ∀ 𝑎𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ∧ ∀ 𝑎𝑐 ( 𝑎 ) = ( 𝑎 𝐺 ( ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ) → ( ( dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀ 𝑎 ∈ ( dom 𝑔 ∩ dom ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( dom 𝑔 ∩ dom ) ) )
61 28 60 sylbir ( ( ∃ 𝑏 ( 𝑔 Fn 𝑏 ∧ ( 𝑏𝐴 ∧ ∀ 𝑎𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ∀ 𝑎𝑏 ( 𝑔𝑎 ) = ( 𝑎 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ∧ ∃ 𝑐 ( Fn 𝑐 ∧ ( 𝑐𝐴 ∧ ∀ 𝑎𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ∧ ∀ 𝑎𝑐 ( 𝑎 ) = ( 𝑎 𝐺 ( ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ) → ( ( dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀ 𝑎 ∈ ( dom 𝑔 ∩ dom ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( dom 𝑔 ∩ dom ) ) )
62 8 27 61 syl2anb ( ( 𝑔𝐵𝐵 ) → ( ( dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀ 𝑎 ∈ ( dom 𝑔 ∩ dom ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( dom 𝑔 ∩ dom ) ) )
63 62 adantr ( ( ( 𝑔𝐵𝐵 ) ∧ 𝑎 ∈ ( dom 𝑔 ∩ dom ) ) → ( ( dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀ 𝑎 ∈ ( dom 𝑔 ∩ dom ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( dom 𝑔 ∩ dom ) ) )
64 preddowncl ( ( ( dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀ 𝑎 ∈ ( dom 𝑔 ∩ dom ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( dom 𝑔 ∩ dom ) ) → ( 𝑎 ∈ ( dom 𝑔 ∩ dom ) → Pred ( 𝑅 , ( dom 𝑔 ∩ dom ) , 𝑎 ) = Pred ( 𝑅 , 𝐴 , 𝑎 ) ) )
65 63 20 64 sylc ( ( ( 𝑔𝐵𝐵 ) ∧ 𝑎 ∈ ( dom 𝑔 ∩ dom ) ) → Pred ( 𝑅 , ( dom 𝑔 ∩ dom ) , 𝑎 ) = Pred ( 𝑅 , 𝐴 , 𝑎 ) )
66 25 65 eqtrid ( ( ( 𝑔𝐵𝐵 ) ∧ 𝑎 ∈ ( dom 𝑔 ∩ dom ) ) → ( ( dom 𝑔 ∩ dom ) ∩ Pred ( 𝑅 , ( dom 𝑔 ∩ dom ) , 𝑎 ) ) = Pred ( 𝑅 , 𝐴 , 𝑎 ) )
67 66 reseq2d ( ( ( 𝑔𝐵𝐵 ) ∧ 𝑎 ∈ ( dom 𝑔 ∩ dom ) ) → ( 𝑔 ↾ ( ( dom 𝑔 ∩ dom ) ∩ Pred ( 𝑅 , ( dom 𝑔 ∩ dom ) , 𝑎 ) ) ) = ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) )
68 22 67 eqtrid ( ( ( 𝑔𝐵𝐵 ) ∧ 𝑎 ∈ ( dom 𝑔 ∩ dom ) ) → ( ( 𝑔 ↾ ( dom 𝑔 ∩ dom ) ) ↾ Pred ( 𝑅 , ( dom 𝑔 ∩ dom ) , 𝑎 ) ) = ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) )
69 68 oveq2d ( ( ( 𝑔𝐵𝐵 ) ∧ 𝑎 ∈ ( dom 𝑔 ∩ dom ) ) → ( 𝑎 𝐺 ( ( 𝑔 ↾ ( dom 𝑔 ∩ dom ) ) ↾ Pred ( 𝑅 , ( dom 𝑔 ∩ dom ) , 𝑎 ) ) ) = ( 𝑎 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) )
70 19 21 69 3eqtr4d ( ( ( 𝑔𝐵𝐵 ) ∧ 𝑎 ∈ ( dom 𝑔 ∩ dom ) ) → ( ( 𝑔 ↾ ( dom 𝑔 ∩ dom ) ) ‘ 𝑎 ) = ( 𝑎 𝐺 ( ( 𝑔 ↾ ( dom 𝑔 ∩ dom ) ) ↾ Pred ( 𝑅 , ( dom 𝑔 ∩ dom ) , 𝑎 ) ) ) )
71 70 ralrimiva ( ( 𝑔𝐵𝐵 ) → ∀ 𝑎 ∈ ( dom 𝑔 ∩ dom ) ( ( 𝑔 ↾ ( dom 𝑔 ∩ dom ) ) ‘ 𝑎 ) = ( 𝑎 𝐺 ( ( 𝑔 ↾ ( dom 𝑔 ∩ dom ) ) ↾ Pred ( 𝑅 , ( dom 𝑔 ∩ dom ) , 𝑎 ) ) ) )
72 6 71 jca ( ( 𝑔𝐵𝐵 ) → ( ( 𝑔 ↾ ( dom 𝑔 ∩ dom ) ) Fn ( dom 𝑔 ∩ dom ) ∧ ∀ 𝑎 ∈ ( dom 𝑔 ∩ dom ) ( ( 𝑔 ↾ ( dom 𝑔 ∩ dom ) ) ‘ 𝑎 ) = ( 𝑎 𝐺 ( ( 𝑔 ↾ ( dom 𝑔 ∩ dom ) ) ↾ Pred ( 𝑅 , ( dom 𝑔 ∩ dom ) , 𝑎 ) ) ) ) )