Metamath Proof Explorer

Theorem wfrlem4

Description: Lemma for well-founded recursion. Properties of the restriction of an acceptable function to the domain of another one. (Contributed by Scott Fenton, 21-Apr-2011) (Revised by AV, 18-Jul-2022)

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

Proof

Step Hyp Ref Expression
1 wfrlem4.2 ⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
2 1 wfrlem2 ⊢ ( 𝑔 ∈ 𝐵 → 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 wfrlem1 ⊢ 𝐵 = { 𝑔 ∣ ∃ 𝑏 ( 𝑔 Fn 𝑏 ∧ ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ∀ 𝑎 ∈ 𝑏 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) }
8 7 abeq2i ⊢ ( 𝑔 ∈ 𝐵 ↔ ∃ 𝑏 ( 𝑔 Fn 𝑏 ∧ ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ∀ 𝑎 ∈ 𝑏 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) )
9 fndm ⊢ ( 𝑔 Fn 𝑏 → dom 𝑔 = 𝑏 )
10 9 raleqdv ⊢ ( 𝑔 Fn 𝑏 → ( ∀ 𝑎 ∈ dom 𝑔 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ↔ ∀ 𝑎 ∈ 𝑏 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) )
11 10 biimpar ⊢ ( ( 𝑔 Fn 𝑏 ∧ ∀ 𝑎 ∈ 𝑏 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) → ∀ 𝑎 ∈ dom 𝑔 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) )
12 rsp ⊢ ( ∀ 𝑎 ∈ dom 𝑔 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) → ( 𝑎 ∈ dom 𝑔 → ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) )
13 11 12 syl ⊢ ( ( 𝑔 Fn 𝑏 ∧ ∀ 𝑎 ∈ 𝑏 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) → ( 𝑎 ∈ dom 𝑔 → ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) )
14 13 3adant2 ⊢ ( ( 𝑔 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 fvres ⊢ ( 𝑎 ∈ ( dom 𝑔 ∩ dom ℎ ) → ( ( 𝑔 ↾ ( dom 𝑔 ∩ dom ℎ ) ) ‘ 𝑎 ) = ( 𝑔 ‘ 𝑎 ) )
21 20 adantl ⊢ ( ( ( 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ 𝑎 ∈ ( 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 wfrlem1 ⊢ 𝐵 = { ℎ ∣ ∃ 𝑐 ( ℎ Fn 𝑐 ∧ ( 𝑐 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ∧ ∀ 𝑎 ∈ 𝑐 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) }
27 26 abeq2i ⊢ ( ℎ ∈ 𝐵 ↔ ∃ 𝑐 ( ℎ Fn 𝑐 ∧ ( 𝑐 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ∧ ∀ 𝑎 ∈ 𝑐 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) )
28 3an6 ⊢ ( ( ( 𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐 ) ∧ ( ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ( 𝑐 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ) ∧ ( ∀ 𝑎 ∈ 𝑏 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ∧ ∀ 𝑎 ∈ 𝑐 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ) ↔ ( ( 𝑔 Fn 𝑏 ∧ ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ∀ 𝑎 ∈ 𝑏 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ∧ ( ℎ Fn 𝑐 ∧ ( 𝑐 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ∧ ∀ 𝑎 ∈ 𝑐 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ) )
29 28 2exbii ⊢ ( ∃ 𝑏 ∃ 𝑐 ( ( 𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐 ) ∧ ( ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ( 𝑐 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ) ∧ ( ∀ 𝑎 ∈ 𝑏 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ∧ ∀ 𝑎 ∈ 𝑐 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ) ↔ ∃ 𝑏 ∃ 𝑐 ( ( 𝑔 Fn 𝑏 ∧ ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ∀ 𝑎 ∈ 𝑏 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ∧ ( ℎ Fn 𝑐 ∧ ( 𝑐 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ∧ ∀ 𝑎 ∈ 𝑐 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ) )
30 exdistrv ⊢ ( ∃ 𝑏 ∃ 𝑐 ( ( 𝑔 Fn 𝑏 ∧ ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ∀ 𝑎 ∈ 𝑏 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ∧ ( ℎ Fn 𝑐 ∧ ( 𝑐 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ∧ ∀ 𝑎 ∈ 𝑐 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ) ↔ ( ∃ 𝑏 ( 𝑔 Fn 𝑏 ∧ ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ∀ 𝑎 ∈ 𝑏 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ∧ ∃ 𝑐 ( ℎ Fn 𝑐 ∧ ( 𝑐 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ∧ ∀ 𝑎 ∈ 𝑐 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ) )
31 29 30 bitri ⊢ ( ∃ 𝑏 ∃ 𝑐 ( ( 𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐 ) ∧ ( ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ( 𝑐 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ) ∧ ( ∀ 𝑎 ∈ 𝑏 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ∧ ∀ 𝑎 ∈ 𝑐 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ) ↔ ( ∃ 𝑏 ( 𝑔 Fn 𝑏 ∧ ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ∀ 𝑎 ∈ 𝑏 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ∧ ∃ 𝑐 ( ℎ Fn 𝑐 ∧ ( 𝑐 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ∧ ∀ 𝑎 ∈ 𝑐 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ) )
32 ssinss1 ⊢ ( 𝑏 ⊆ 𝐴 → ( 𝑏 ∩ 𝑐 ) ⊆ 𝐴 )
33 32 ad2antrr ⊢ ( ( ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑏 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 47 ad2ant2l ⊢ ( ( ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ( 𝑐 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ) → ∀ 𝑎 ∈ ( 𝑏 ∩ 𝑐 ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( 𝑏 ∩ 𝑐 ) )
49 33 48 jca ⊢ ( ( ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ( 𝑐 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ) → ( ( 𝑏 ∩ 𝑐 ) ⊆ 𝐴 ∧ ∀ 𝑎 ∈ ( 𝑏 ∩ 𝑐 ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( 𝑏 ∩ 𝑐 ) ) )
50 fndm ⊢ ( ℎ Fn 𝑐 → dom ℎ = 𝑐 )
51 9 50 ineqan12d ⊢ ( ( 𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐 ) → ( dom 𝑔 ∩ dom ℎ ) = ( 𝑏 ∩ 𝑐 ) )
52 sseq1 ⊢ ( ( dom 𝑔 ∩ dom ℎ ) = ( 𝑏 ∩ 𝑐 ) → ( ( dom 𝑔 ∩ dom ℎ ) ⊆ 𝐴 ↔ ( 𝑏 ∩ 𝑐 ) ⊆ 𝐴 ) )
53 sseq2 ⊢ ( ( dom 𝑔 ∩ dom ℎ ) = ( 𝑏 ∩ 𝑐 ) → ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( dom 𝑔 ∩ dom ℎ ) ↔ Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( 𝑏 ∩ 𝑐 ) ) )
54 53 raleqbi1dv ⊢ ( ( dom 𝑔 ∩ dom ℎ ) = ( 𝑏 ∩ 𝑐 ) → ( ∀ 𝑎 ∈ ( dom 𝑔 ∩ dom ℎ ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( dom 𝑔 ∩ dom ℎ ) ↔ ∀ 𝑎 ∈ ( 𝑏 ∩ 𝑐 ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( 𝑏 ∩ 𝑐 ) ) )
55 52 54 anbi12d ⊢ ( ( dom 𝑔 ∩ dom ℎ ) = ( 𝑏 ∩ 𝑐 ) → ( ( ( dom 𝑔 ∩ dom ℎ ) ⊆ 𝐴 ∧ ∀ 𝑎 ∈ ( dom 𝑔 ∩ dom ℎ ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( dom 𝑔 ∩ dom ℎ ) ) ↔ ( ( 𝑏 ∩ 𝑐 ) ⊆ 𝐴 ∧ ∀ 𝑎 ∈ ( 𝑏 ∩ 𝑐 ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( 𝑏 ∩ 𝑐 ) ) ) )
56 55 imbi2d ⊢ ( ( dom 𝑔 ∩ dom ℎ ) = ( 𝑏 ∩ 𝑐 ) → ( ( ( ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ( 𝑐 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ) → ( ( dom 𝑔 ∩ dom ℎ ) ⊆ 𝐴 ∧ ∀ 𝑎 ∈ ( dom 𝑔 ∩ dom ℎ ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( dom 𝑔 ∩ dom ℎ ) ) ) ↔ ( ( ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ( 𝑐 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ) → ( ( 𝑏 ∩ 𝑐 ) ⊆ 𝐴 ∧ ∀ 𝑎 ∈ ( 𝑏 ∩ 𝑐 ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( 𝑏 ∩ 𝑐 ) ) ) ) )
57 51 56 syl ⊢ ( ( 𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐 ) → ( ( ( ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ( 𝑐 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ) → ( ( dom 𝑔 ∩ dom ℎ ) ⊆ 𝐴 ∧ ∀ 𝑎 ∈ ( dom 𝑔 ∩ dom ℎ ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( dom 𝑔 ∩ dom ℎ ) ) ) ↔ ( ( ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ( 𝑐 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ) → ( ( 𝑏 ∩ 𝑐 ) ⊆ 𝐴 ∧ ∀ 𝑎 ∈ ( 𝑏 ∩ 𝑐 ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( 𝑏 ∩ 𝑐 ) ) ) ) )
58 49 57 mpbiri ⊢ ( ( 𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐 ) → ( ( ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ( 𝑐 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ) → ( ( dom 𝑔 ∩ dom ℎ ) ⊆ 𝐴 ∧ ∀ 𝑎 ∈ ( dom 𝑔 ∩ dom ℎ ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( dom 𝑔 ∩ dom ℎ ) ) ) )
59 58 imp ⊢ ( ( ( 𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐 ) ∧ ( ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ( 𝑐 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ) ) → ( ( dom 𝑔 ∩ dom ℎ ) ⊆ 𝐴 ∧ ∀ 𝑎 ∈ ( dom 𝑔 ∩ dom ℎ ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( dom 𝑔 ∩ dom ℎ ) ) )
60 59 3adant3 ⊢ ( ( ( 𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐 ) ∧ ( ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ( 𝑐 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ) ∧ ( ∀ 𝑎 ∈ 𝑏 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ∧ ∀ 𝑎 ∈ 𝑐 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ) → ( ( dom 𝑔 ∩ dom ℎ ) ⊆ 𝐴 ∧ ∀ 𝑎 ∈ ( dom 𝑔 ∩ dom ℎ ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( dom 𝑔 ∩ dom ℎ ) ) )
61 60 exlimivv ⊢ ( ∃ 𝑏 ∃ 𝑐 ( ( 𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐 ) ∧ ( ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ( 𝑐 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ) ∧ ( ∀ 𝑎 ∈ 𝑏 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ∧ ∀ 𝑎 ∈ 𝑐 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ) → ( ( dom 𝑔 ∩ dom ℎ ) ⊆ 𝐴 ∧ ∀ 𝑎 ∈ ( dom 𝑔 ∩ dom ℎ ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( dom 𝑔 ∩ dom ℎ ) ) )
62 31 61 sylbir ⊢ ( ( ∃ 𝑏 ( 𝑔 Fn 𝑏 ∧ ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑏 ) ∧ ∀ 𝑎 ∈ 𝑏 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ∧ ∃ 𝑐 ( ℎ Fn 𝑐 ∧ ( 𝑐 ⊆ 𝐴 ∧ ∀ 𝑎 ∈ 𝑐 Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝑐 ) ∧ ∀ 𝑎 ∈ 𝑐 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) ) ) → ( ( dom 𝑔 ∩ dom ℎ ) ⊆ 𝐴 ∧ ∀ 𝑎 ∈ ( dom 𝑔 ∩ dom ℎ ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( dom 𝑔 ∩ dom ℎ ) ) )
63 8 27 62 syl2anb ⊢ ( ( 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) → ( ( dom 𝑔 ∩ dom ℎ ) ⊆ 𝐴 ∧ ∀ 𝑎 ∈ ( dom 𝑔 ∩ dom ℎ ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( dom 𝑔 ∩ dom ℎ ) ) )
64 63 adantr ⊢ ( ( ( 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ 𝑎 ∈ ( dom 𝑔 ∩ dom ℎ ) ) → ( ( dom 𝑔 ∩ dom ℎ ) ⊆ 𝐴 ∧ ∀ 𝑎 ∈ ( dom 𝑔 ∩ dom ℎ ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( dom 𝑔 ∩ dom ℎ ) ) )
65 simpr ⊢ ( ( ( 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ 𝑎 ∈ ( dom 𝑔 ∩ dom ℎ ) ) → 𝑎 ∈ ( dom 𝑔 ∩ dom ℎ ) )
66 preddowncl ⊢ ( ( ( dom 𝑔 ∩ dom ℎ ) ⊆ 𝐴 ∧ ∀ 𝑎 ∈ ( dom 𝑔 ∩ dom ℎ ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( dom 𝑔 ∩ dom ℎ ) ) → ( 𝑎 ∈ ( dom 𝑔 ∩ dom ℎ ) → Pred ( 𝑅 , ( dom 𝑔 ∩ dom ℎ ) , 𝑎 ) = Pred ( 𝑅 , 𝐴 , 𝑎 ) ) )
67 64 65 66 sylc ⊢ ( ( ( 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ 𝑎 ∈ ( dom 𝑔 ∩ dom ℎ ) ) → Pred ( 𝑅 , ( dom 𝑔 ∩ dom ℎ ) , 𝑎 ) = Pred ( 𝑅 , 𝐴 , 𝑎 ) )
68 25 67 syl5eq ⊢ ( ( ( 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ 𝑎 ∈ ( dom 𝑔 ∩ dom ℎ ) ) → ( ( dom 𝑔 ∩ dom ℎ ) ∩ Pred ( 𝑅 , ( dom 𝑔 ∩ dom ℎ ) , 𝑎 ) ) = Pred ( 𝑅 , 𝐴 , 𝑎 ) )
69 68 reseq2d ⊢ ( ( ( 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ 𝑎 ∈ ( dom 𝑔 ∩ dom ℎ ) ) → ( 𝑔 ↾ ( ( dom 𝑔 ∩ dom ℎ ) ∩ Pred ( 𝑅 , ( dom 𝑔 ∩ dom ℎ ) , 𝑎 ) ) ) = ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) )
70 22 69 syl5eq ⊢ ( ( ( 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ 𝑎 ∈ ( dom 𝑔 ∩ dom ℎ ) ) → ( ( 𝑔 ↾ ( dom 𝑔 ∩ dom ℎ ) ) ↾ Pred ( 𝑅 , ( dom 𝑔 ∩ dom ℎ ) , 𝑎 ) ) = ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) )
71 70 fveq2d ⊢ ( ( ( 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ 𝑎 ∈ ( dom 𝑔 ∩ dom ℎ ) ) → ( 𝐹 ‘ ( ( 𝑔 ↾ ( dom 𝑔 ∩ dom ℎ ) ) ↾ Pred ( 𝑅 , ( dom 𝑔 ∩ dom ℎ ) , 𝑎 ) ) ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) ) )
72 19 21 71 3eqtr4d ⊢ ( ( ( 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ 𝑎 ∈ ( dom 𝑔 ∩ dom ℎ ) ) → ( ( 𝑔 ↾ ( dom 𝑔 ∩ dom ℎ ) ) ‘ 𝑎 ) = ( 𝐹 ‘ ( ( 𝑔 ↾ ( dom 𝑔 ∩ dom ℎ ) ) ↾ Pred ( 𝑅 , ( dom 𝑔 ∩ dom ℎ ) , 𝑎 ) ) ) )
73 72 ralrimiva ⊢ ( ( 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) → ∀ 𝑎 ∈ ( dom 𝑔 ∩ dom ℎ ) ( ( 𝑔 ↾ ( dom 𝑔 ∩ dom ℎ ) ) ‘ 𝑎 ) = ( 𝐹 ‘ ( ( 𝑔 ↾ ( dom 𝑔 ∩ dom ℎ ) ) ↾ Pred ( 𝑅 , ( dom 𝑔 ∩ dom ℎ ) , 𝑎 ) ) ) )
74 6 73 jca ⊢ ( ( 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) → ( ( 𝑔 ↾ ( dom 𝑔 ∩ dom ℎ ) ) Fn ( dom 𝑔 ∩ dom ℎ ) ∧ ∀ 𝑎 ∈ ( dom 𝑔 ∩ dom ℎ ) ( ( 𝑔 ↾ ( dom 𝑔 ∩ dom ℎ ) ) ‘ 𝑎 ) = ( 𝐹 ‘ ( ( 𝑔 ↾ ( dom 𝑔 ∩ dom ℎ ) ) ↾ Pred ( 𝑅 , ( dom 𝑔 ∩ dom ℎ ) , 𝑎 ) ) ) ) )