# 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 ${⊢}{B}=\left\{{f}|\exists {x}\phantom{\rule{.4em}{0ex}}\left({f}Fn{x}\wedge \left({x}\subseteq {A}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{y}\right)\subseteq {x}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)={F}\left({{f}↾}_{Pred\left({R},{A},{y}\right)}\right)\right)\right\}$
Assertion wfrlem4 ${⊢}\left({g}\in {B}\wedge {h}\in {B}\right)\to \left(\left({{g}↾}_{\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)}\right)Fn\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\wedge \forall {a}\in \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\phantom{\rule{.4em}{0ex}}\left({{g}↾}_{\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)}\right)\left({a}\right)={F}\left({\left({{g}↾}_{\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)}\right)↾}_{Pred\left({R},\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right),{a}\right)}\right)\right)$

### Proof

Step Hyp Ref Expression
1 wfrlem4.2 ${⊢}{B}=\left\{{f}|\exists {x}\phantom{\rule{.4em}{0ex}}\left({f}Fn{x}\wedge \left({x}\subseteq {A}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{y}\right)\subseteq {x}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)={F}\left({{f}↾}_{Pred\left({R},{A},{y}\right)}\right)\right)\right\}$
2 1 wfrlem2 ${⊢}{g}\in {B}\to \mathrm{Fun}{g}$
3 2 funfnd ${⊢}{g}\in {B}\to {g}Fn\mathrm{dom}{g}$
4 fnresin1 ${⊢}{g}Fn\mathrm{dom}{g}\to \left({{g}↾}_{\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)}\right)Fn\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)$
5 3 4 syl ${⊢}{g}\in {B}\to \left({{g}↾}_{\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)}\right)Fn\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)$
6 5 adantr ${⊢}\left({g}\in {B}\wedge {h}\in {B}\right)\to \left({{g}↾}_{\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)}\right)Fn\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)$
7 1 wfrlem1 ${⊢}{B}=\left\{{g}|\exists {b}\phantom{\rule{.4em}{0ex}}\left({g}Fn{b}\wedge \left({b}\subseteq {A}\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\right)\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{Pred\left({R},{A},{a}\right)}\right)\right)\right\}$
8 7 abeq2i ${⊢}{g}\in {B}↔\exists {b}\phantom{\rule{.4em}{0ex}}\left({g}Fn{b}\wedge \left({b}\subseteq {A}\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\right)\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{Pred\left({R},{A},{a}\right)}\right)\right)$
9 fndm ${⊢}{g}Fn{b}\to \mathrm{dom}{g}={b}$
10 9 raleqdv ${⊢}{g}Fn{b}\to \left(\forall {a}\in \mathrm{dom}{g}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{Pred\left({R},{A},{a}\right)}\right)↔\forall {a}\in {b}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{Pred\left({R},{A},{a}\right)}\right)\right)$
11 10 biimpar ${⊢}\left({g}Fn{b}\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{Pred\left({R},{A},{a}\right)}\right)\right)\to \forall {a}\in \mathrm{dom}{g}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{Pred\left({R},{A},{a}\right)}\right)$
12 rsp ${⊢}\forall {a}\in \mathrm{dom}{g}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{Pred\left({R},{A},{a}\right)}\right)\to \left({a}\in \mathrm{dom}{g}\to {g}\left({a}\right)={F}\left({{g}↾}_{Pred\left({R},{A},{a}\right)}\right)\right)$
13 11 12 syl ${⊢}\left({g}Fn{b}\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{Pred\left({R},{A},{a}\right)}\right)\right)\to \left({a}\in \mathrm{dom}{g}\to {g}\left({a}\right)={F}\left({{g}↾}_{Pred\left({R},{A},{a}\right)}\right)\right)$
14 13 3adant2 ${⊢}\left({g}Fn{b}\wedge \left({b}\subseteq {A}\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\right)\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{Pred\left({R},{A},{a}\right)}\right)\right)\to \left({a}\in \mathrm{dom}{g}\to {g}\left({a}\right)={F}\left({{g}↾}_{Pred\left({R},{A},{a}\right)}\right)\right)$
15 14 exlimiv ${⊢}\exists {b}\phantom{\rule{.4em}{0ex}}\left({g}Fn{b}\wedge \left({b}\subseteq {A}\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\right)\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{Pred\left({R},{A},{a}\right)}\right)\right)\to \left({a}\in \mathrm{dom}{g}\to {g}\left({a}\right)={F}\left({{g}↾}_{Pred\left({R},{A},{a}\right)}\right)\right)$
16 8 15 sylbi ${⊢}{g}\in {B}\to \left({a}\in \mathrm{dom}{g}\to {g}\left({a}\right)={F}\left({{g}↾}_{Pred\left({R},{A},{a}\right)}\right)\right)$
17 elinel1 ${⊢}{a}\in \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\to {a}\in \mathrm{dom}{g}$
18 16 17 impel ${⊢}\left({g}\in {B}\wedge {a}\in \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\right)\to {g}\left({a}\right)={F}\left({{g}↾}_{Pred\left({R},{A},{a}\right)}\right)$
19 18 adantlr ${⊢}\left(\left({g}\in {B}\wedge {h}\in {B}\right)\wedge {a}\in \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\right)\to {g}\left({a}\right)={F}\left({{g}↾}_{Pred\left({R},{A},{a}\right)}\right)$
20 fvres ${⊢}{a}\in \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\to \left({{g}↾}_{\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)}\right)\left({a}\right)={g}\left({a}\right)$
21 20 adantl ${⊢}\left(\left({g}\in {B}\wedge {h}\in {B}\right)\wedge {a}\in \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\right)\to \left({{g}↾}_{\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)}\right)\left({a}\right)={g}\left({a}\right)$
22 resres ${⊢}{\left({{g}↾}_{\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)}\right)↾}_{Pred\left({R},\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right),{a}\right)}={{g}↾}_{\left(\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\cap Pred\left({R},\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right),{a}\right)\right)}$
23 predss ${⊢}Pred\left({R},\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right),{a}\right)\subseteq \mathrm{dom}{g}\cap \mathrm{dom}{h}$
24 sseqin2 ${⊢}Pred\left({R},\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right),{a}\right)\subseteq \mathrm{dom}{g}\cap \mathrm{dom}{h}↔\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\cap Pred\left({R},\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right),{a}\right)=Pred\left({R},\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right),{a}\right)$
25 23 24 mpbi ${⊢}\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\cap Pred\left({R},\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right),{a}\right)=Pred\left({R},\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right),{a}\right)$
26 1 wfrlem1 ${⊢}{B}=\left\{{h}|\exists {c}\phantom{\rule{.4em}{0ex}}\left({h}Fn{c}\wedge \left({c}\subseteq {A}\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {c}\right)\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{Pred\left({R},{A},{a}\right)}\right)\right)\right\}$
27 26 abeq2i ${⊢}{h}\in {B}↔\exists {c}\phantom{\rule{.4em}{0ex}}\left({h}Fn{c}\wedge \left({c}\subseteq {A}\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {c}\right)\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{Pred\left({R},{A},{a}\right)}\right)\right)$
28 3an6 ${⊢}\left(\left({g}Fn{b}\wedge {h}Fn{c}\right)\wedge \left(\left({b}\subseteq {A}\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\right)\wedge \left({c}\subseteq {A}\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {c}\right)\right)\wedge \left(\forall {a}\in {b}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{Pred\left({R},{A},{a}\right)}\right)\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{Pred\left({R},{A},{a}\right)}\right)\right)\right)↔\left(\left({g}Fn{b}\wedge \left({b}\subseteq {A}\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\right)\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{Pred\left({R},{A},{a}\right)}\right)\right)\wedge \left({h}Fn{c}\wedge \left({c}\subseteq {A}\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {c}\right)\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{Pred\left({R},{A},{a}\right)}\right)\right)\right)$
29 28 2exbii ${⊢}\exists {b}\phantom{\rule{.4em}{0ex}}\exists {c}\phantom{\rule{.4em}{0ex}}\left(\left({g}Fn{b}\wedge {h}Fn{c}\right)\wedge \left(\left({b}\subseteq {A}\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\right)\wedge \left({c}\subseteq {A}\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {c}\right)\right)\wedge \left(\forall {a}\in {b}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{Pred\left({R},{A},{a}\right)}\right)\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{Pred\left({R},{A},{a}\right)}\right)\right)\right)↔\exists {b}\phantom{\rule{.4em}{0ex}}\exists {c}\phantom{\rule{.4em}{0ex}}\left(\left({g}Fn{b}\wedge \left({b}\subseteq {A}\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\right)\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{Pred\left({R},{A},{a}\right)}\right)\right)\wedge \left({h}Fn{c}\wedge \left({c}\subseteq {A}\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {c}\right)\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{Pred\left({R},{A},{a}\right)}\right)\right)\right)$
30 exdistrv ${⊢}\exists {b}\phantom{\rule{.4em}{0ex}}\exists {c}\phantom{\rule{.4em}{0ex}}\left(\left({g}Fn{b}\wedge \left({b}\subseteq {A}\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\right)\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{Pred\left({R},{A},{a}\right)}\right)\right)\wedge \left({h}Fn{c}\wedge \left({c}\subseteq {A}\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {c}\right)\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{Pred\left({R},{A},{a}\right)}\right)\right)\right)↔\left(\exists {b}\phantom{\rule{.4em}{0ex}}\left({g}Fn{b}\wedge \left({b}\subseteq {A}\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\right)\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{Pred\left({R},{A},{a}\right)}\right)\right)\wedge \exists {c}\phantom{\rule{.4em}{0ex}}\left({h}Fn{c}\wedge \left({c}\subseteq {A}\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {c}\right)\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{Pred\left({R},{A},{a}\right)}\right)\right)\right)$
31 29 30 bitri ${⊢}\exists {b}\phantom{\rule{.4em}{0ex}}\exists {c}\phantom{\rule{.4em}{0ex}}\left(\left({g}Fn{b}\wedge {h}Fn{c}\right)\wedge \left(\left({b}\subseteq {A}\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\right)\wedge \left({c}\subseteq {A}\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {c}\right)\right)\wedge \left(\forall {a}\in {b}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{Pred\left({R},{A},{a}\right)}\right)\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{Pred\left({R},{A},{a}\right)}\right)\right)\right)↔\left(\exists {b}\phantom{\rule{.4em}{0ex}}\left({g}Fn{b}\wedge \left({b}\subseteq {A}\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\right)\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{Pred\left({R},{A},{a}\right)}\right)\right)\wedge \exists {c}\phantom{\rule{.4em}{0ex}}\left({h}Fn{c}\wedge \left({c}\subseteq {A}\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {c}\right)\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{Pred\left({R},{A},{a}\right)}\right)\right)\right)$
32 ssinss1 ${⊢}{b}\subseteq {A}\to {b}\cap {c}\subseteq {A}$
33 32 ad2antrr ${⊢}\left(\left({b}\subseteq {A}\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\right)\wedge \left({c}\subseteq {A}\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {c}\right)\right)\to {b}\cap {c}\subseteq {A}$
34 nfra1 ${⊢}Ⅎ{a}\phantom{\rule{.4em}{0ex}}\forall {a}\in {b}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}$
35 nfra1 ${⊢}Ⅎ{a}\phantom{\rule{.4em}{0ex}}\forall {a}\in {c}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {c}$
36 34 35 nfan ${⊢}Ⅎ{a}\phantom{\rule{.4em}{0ex}}\left(\forall {a}\in {b}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {c}\right)$
37 elinel1 ${⊢}{a}\in \left({b}\cap {c}\right)\to {a}\in {b}$
38 rsp ${⊢}\forall {a}\in {b}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\to \left({a}\in {b}\to Pred\left({R},{A},{a}\right)\subseteq {b}\right)$
39 37 38 syl5com ${⊢}{a}\in \left({b}\cap {c}\right)\to \left(\forall {a}\in {b}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\to Pred\left({R},{A},{a}\right)\subseteq {b}\right)$
40 elinel2 ${⊢}{a}\in \left({b}\cap {c}\right)\to {a}\in {c}$
41 rsp ${⊢}\forall {a}\in {c}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {c}\to \left({a}\in {c}\to Pred\left({R},{A},{a}\right)\subseteq {c}\right)$
42 40 41 syl5com ${⊢}{a}\in \left({b}\cap {c}\right)\to \left(\forall {a}\in {c}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {c}\to Pred\left({R},{A},{a}\right)\subseteq {c}\right)$
43 39 42 anim12d ${⊢}{a}\in \left({b}\cap {c}\right)\to \left(\left(\forall {a}\in {b}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {c}\right)\to \left(Pred\left({R},{A},{a}\right)\subseteq {b}\wedge Pred\left({R},{A},{a}\right)\subseteq {c}\right)\right)$
44 ssin ${⊢}\left(Pred\left({R},{A},{a}\right)\subseteq {b}\wedge Pred\left({R},{A},{a}\right)\subseteq {c}\right)↔Pred\left({R},{A},{a}\right)\subseteq {b}\cap {c}$
45 44 biimpi ${⊢}\left(Pred\left({R},{A},{a}\right)\subseteq {b}\wedge Pred\left({R},{A},{a}\right)\subseteq {c}\right)\to Pred\left({R},{A},{a}\right)\subseteq {b}\cap {c}$
46 43 45 syl6com ${⊢}\left(\forall {a}\in {b}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {c}\right)\to \left({a}\in \left({b}\cap {c}\right)\to Pred\left({R},{A},{a}\right)\subseteq {b}\cap {c}\right)$
47 36 46 ralrimi ${⊢}\left(\forall {a}\in {b}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {c}\right)\to \forall {a}\in \left({b}\cap {c}\right)\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\cap {c}$
48 47 ad2ant2l ${⊢}\left(\left({b}\subseteq {A}\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\right)\wedge \left({c}\subseteq {A}\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {c}\right)\right)\to \forall {a}\in \left({b}\cap {c}\right)\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\cap {c}$
49 33 48 jca ${⊢}\left(\left({b}\subseteq {A}\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\right)\wedge \left({c}\subseteq {A}\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {c}\right)\right)\to \left({b}\cap {c}\subseteq {A}\wedge \forall {a}\in \left({b}\cap {c}\right)\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\cap {c}\right)$
50 fndm ${⊢}{h}Fn{c}\to \mathrm{dom}{h}={c}$
51 9 50 ineqan12d ${⊢}\left({g}Fn{b}\wedge {h}Fn{c}\right)\to \mathrm{dom}{g}\cap \mathrm{dom}{h}={b}\cap {c}$
52 sseq1 ${⊢}\mathrm{dom}{g}\cap \mathrm{dom}{h}={b}\cap {c}\to \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\subseteq {A}↔{b}\cap {c}\subseteq {A}\right)$
53 sseq2 ${⊢}\mathrm{dom}{g}\cap \mathrm{dom}{h}={b}\cap {c}\to \left(Pred\left({R},{A},{a}\right)\subseteq \mathrm{dom}{g}\cap \mathrm{dom}{h}↔Pred\left({R},{A},{a}\right)\subseteq {b}\cap {c}\right)$
54 53 raleqbi1dv ${⊢}\mathrm{dom}{g}\cap \mathrm{dom}{h}={b}\cap {c}\to \left(\forall {a}\in \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq \mathrm{dom}{g}\cap \mathrm{dom}{h}↔\forall {a}\in \left({b}\cap {c}\right)\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\cap {c}\right)$
55 52 54 anbi12d ${⊢}\mathrm{dom}{g}\cap \mathrm{dom}{h}={b}\cap {c}\to \left(\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\subseteq {A}\wedge \forall {a}\in \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq \mathrm{dom}{g}\cap \mathrm{dom}{h}\right)↔\left({b}\cap {c}\subseteq {A}\wedge \forall {a}\in \left({b}\cap {c}\right)\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\cap {c}\right)\right)$
56 55 imbi2d ${⊢}\mathrm{dom}{g}\cap \mathrm{dom}{h}={b}\cap {c}\to \left(\left(\left(\left({b}\subseteq {A}\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\right)\wedge \left({c}\subseteq {A}\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {c}\right)\right)\to \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\subseteq {A}\wedge \forall {a}\in \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq \mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\right)↔\left(\left(\left({b}\subseteq {A}\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\right)\wedge \left({c}\subseteq {A}\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {c}\right)\right)\to \left({b}\cap {c}\subseteq {A}\wedge \forall {a}\in \left({b}\cap {c}\right)\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\cap {c}\right)\right)\right)$
57 51 56 syl ${⊢}\left({g}Fn{b}\wedge {h}Fn{c}\right)\to \left(\left(\left(\left({b}\subseteq {A}\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\right)\wedge \left({c}\subseteq {A}\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {c}\right)\right)\to \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\subseteq {A}\wedge \forall {a}\in \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq \mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\right)↔\left(\left(\left({b}\subseteq {A}\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\right)\wedge \left({c}\subseteq {A}\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {c}\right)\right)\to \left({b}\cap {c}\subseteq {A}\wedge \forall {a}\in \left({b}\cap {c}\right)\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\cap {c}\right)\right)\right)$
58 49 57 mpbiri ${⊢}\left({g}Fn{b}\wedge {h}Fn{c}\right)\to \left(\left(\left({b}\subseteq {A}\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\right)\wedge \left({c}\subseteq {A}\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {c}\right)\right)\to \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\subseteq {A}\wedge \forall {a}\in \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq \mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\right)$
59 58 imp ${⊢}\left(\left({g}Fn{b}\wedge {h}Fn{c}\right)\wedge \left(\left({b}\subseteq {A}\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\right)\wedge \left({c}\subseteq {A}\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {c}\right)\right)\right)\to \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\subseteq {A}\wedge \forall {a}\in \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq \mathrm{dom}{g}\cap \mathrm{dom}{h}\right)$
60 59 3adant3 ${⊢}\left(\left({g}Fn{b}\wedge {h}Fn{c}\right)\wedge \left(\left({b}\subseteq {A}\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\right)\wedge \left({c}\subseteq {A}\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {c}\right)\right)\wedge \left(\forall {a}\in {b}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{Pred\left({R},{A},{a}\right)}\right)\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{Pred\left({R},{A},{a}\right)}\right)\right)\right)\to \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\subseteq {A}\wedge \forall {a}\in \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq \mathrm{dom}{g}\cap \mathrm{dom}{h}\right)$
61 60 exlimivv ${⊢}\exists {b}\phantom{\rule{.4em}{0ex}}\exists {c}\phantom{\rule{.4em}{0ex}}\left(\left({g}Fn{b}\wedge {h}Fn{c}\right)\wedge \left(\left({b}\subseteq {A}\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\right)\wedge \left({c}\subseteq {A}\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {c}\right)\right)\wedge \left(\forall {a}\in {b}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{Pred\left({R},{A},{a}\right)}\right)\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{Pred\left({R},{A},{a}\right)}\right)\right)\right)\to \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\subseteq {A}\wedge \forall {a}\in \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq \mathrm{dom}{g}\cap \mathrm{dom}{h}\right)$
62 31 61 sylbir ${⊢}\left(\exists {b}\phantom{\rule{.4em}{0ex}}\left({g}Fn{b}\wedge \left({b}\subseteq {A}\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {b}\right)\wedge \forall {a}\in {b}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{Pred\left({R},{A},{a}\right)}\right)\right)\wedge \exists {c}\phantom{\rule{.4em}{0ex}}\left({h}Fn{c}\wedge \left({c}\subseteq {A}\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq {c}\right)\wedge \forall {a}\in {c}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{Pred\left({R},{A},{a}\right)}\right)\right)\right)\to \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\subseteq {A}\wedge \forall {a}\in \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq \mathrm{dom}{g}\cap \mathrm{dom}{h}\right)$
63 8 27 62 syl2anb ${⊢}\left({g}\in {B}\wedge {h}\in {B}\right)\to \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\subseteq {A}\wedge \forall {a}\in \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq \mathrm{dom}{g}\cap \mathrm{dom}{h}\right)$
64 63 adantr ${⊢}\left(\left({g}\in {B}\wedge {h}\in {B}\right)\wedge {a}\in \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\right)\to \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\subseteq {A}\wedge \forall {a}\in \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq \mathrm{dom}{g}\cap \mathrm{dom}{h}\right)$
65 simpr ${⊢}\left(\left({g}\in {B}\wedge {h}\in {B}\right)\wedge {a}\in \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\right)\to {a}\in \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)$
66 preddowncl ${⊢}\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\subseteq {A}\wedge \forall {a}\in \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{a}\right)\subseteq \mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\to \left({a}\in \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\to Pred\left({R},\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right),{a}\right)=Pred\left({R},{A},{a}\right)\right)$
67 64 65 66 sylc ${⊢}\left(\left({g}\in {B}\wedge {h}\in {B}\right)\wedge {a}\in \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\right)\to Pred\left({R},\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right),{a}\right)=Pred\left({R},{A},{a}\right)$
68 25 67 syl5eq ${⊢}\left(\left({g}\in {B}\wedge {h}\in {B}\right)\wedge {a}\in \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\right)\to \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\cap Pred\left({R},\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right),{a}\right)=Pred\left({R},{A},{a}\right)$
69 68 reseq2d ${⊢}\left(\left({g}\in {B}\wedge {h}\in {B}\right)\wedge {a}\in \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\right)\to {{g}↾}_{\left(\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\cap Pred\left({R},\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right),{a}\right)\right)}={{g}↾}_{Pred\left({R},{A},{a}\right)}$
70 22 69 syl5eq ${⊢}\left(\left({g}\in {B}\wedge {h}\in {B}\right)\wedge {a}\in \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\right)\to {\left({{g}↾}_{\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)}\right)↾}_{Pred\left({R},\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right),{a}\right)}={{g}↾}_{Pred\left({R},{A},{a}\right)}$
71 70 fveq2d ${⊢}\left(\left({g}\in {B}\wedge {h}\in {B}\right)\wedge {a}\in \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\right)\to {F}\left({\left({{g}↾}_{\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)}\right)↾}_{Pred\left({R},\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right),{a}\right)}\right)={F}\left({{g}↾}_{Pred\left({R},{A},{a}\right)}\right)$
72 19 21 71 3eqtr4d ${⊢}\left(\left({g}\in {B}\wedge {h}\in {B}\right)\wedge {a}\in \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\right)\to \left({{g}↾}_{\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)}\right)\left({a}\right)={F}\left({\left({{g}↾}_{\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)}\right)↾}_{Pred\left({R},\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right),{a}\right)}\right)$
73 72 ralrimiva ${⊢}\left({g}\in {B}\wedge {h}\in {B}\right)\to \forall {a}\in \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\phantom{\rule{.4em}{0ex}}\left({{g}↾}_{\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)}\right)\left({a}\right)={F}\left({\left({{g}↾}_{\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)}\right)↾}_{Pred\left({R},\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right),{a}\right)}\right)$
74 6 73 jca ${⊢}\left({g}\in {B}\wedge {h}\in {B}\right)\to \left(\left({{g}↾}_{\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)}\right)Fn\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\wedge \forall {a}\in \left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)\phantom{\rule{.4em}{0ex}}\left({{g}↾}_{\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)}\right)\left({a}\right)={F}\left({\left({{g}↾}_{\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right)}\right)↾}_{Pred\left({R},\left(\mathrm{dom}{g}\cap \mathrm{dom}{h}\right),{a}\right)}\right)\right)$