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 eqabri ⊢ ( 𝑔 ∈ 𝐵 ↔ ∃ 𝑏 ( 𝑔 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 eqabri ⊢ ( ℎ ∈ 𝐵 ↔ ∃ 𝑐 ( ℎ 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 ℎ ) , 𝑎 ) ) ) ) )