# Metamath Proof Explorer

## Theorem frrlem2

Description: Lemma for founded recursion. An acceptable function is a function. (Contributed by Paul Chapman, 21-Apr-2012)

Ref Expression
Hypothesis frrlem1.1 ${⊢}{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)={y}{G}\left({{f}↾}_{Pred\left({R},{A},{y}\right)}\right)\right)\right\}$
Assertion frrlem2 ${⊢}{g}\in {B}\to \mathrm{Fun}{g}$

### Proof

Step Hyp Ref Expression
1 frrlem1.1 ${⊢}{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)={y}{G}\left({{f}↾}_{Pred\left({R},{A},{y}\right)}\right)\right)\right\}$
2 1 frrlem1 ${⊢}{B}=\left\{{g}|\exists {z}\phantom{\rule{.4em}{0ex}}\left({g}Fn{z}\wedge \left({z}\subseteq {A}\wedge \forall {w}\in {z}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{w}\right)\subseteq {z}\right)\wedge \forall {w}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({w}\right)={w}{G}\left({{g}↾}_{Pred\left({R},{A},{w}\right)}\right)\right)\right\}$
3 2 abeq2i ${⊢}{g}\in {B}↔\exists {z}\phantom{\rule{.4em}{0ex}}\left({g}Fn{z}\wedge \left({z}\subseteq {A}\wedge \forall {w}\in {z}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{w}\right)\subseteq {z}\right)\wedge \forall {w}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({w}\right)={w}{G}\left({{g}↾}_{Pred\left({R},{A},{w}\right)}\right)\right)$
4 fnfun ${⊢}{g}Fn{z}\to \mathrm{Fun}{g}$
5 4 3ad2ant1 ${⊢}\left({g}Fn{z}\wedge \left({z}\subseteq {A}\wedge \forall {w}\in {z}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{w}\right)\subseteq {z}\right)\wedge \forall {w}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({w}\right)={w}{G}\left({{g}↾}_{Pred\left({R},{A},{w}\right)}\right)\right)\to \mathrm{Fun}{g}$
6 5 exlimiv ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\left({g}Fn{z}\wedge \left({z}\subseteq {A}\wedge \forall {w}\in {z}\phantom{\rule{.4em}{0ex}}Pred\left({R},{A},{w}\right)\subseteq {z}\right)\wedge \forall {w}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({w}\right)={w}{G}\left({{g}↾}_{Pred\left({R},{A},{w}\right)}\right)\right)\to \mathrm{Fun}{g}$
7 3 6 sylbi ${⊢}{g}\in {B}\to \mathrm{Fun}{g}$