# Metamath Proof Explorer

## Theorem tfrlem6

Description: Lemma for transfinite recursion. The union of all acceptable functions is a relation. (Contributed by NM, 8-Aug-1994) (Revised by Mario Carneiro, 9-May-2015)

Ref Expression
Hypothesis tfrlem.1 ${⊢}{A}=\left\{{f}|\exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({f}Fn{x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)={F}\left({{f}↾}_{{y}}\right)\right)\right\}$
Assertion tfrlem6 ${⊢}\mathrm{Rel}\mathrm{recs}\left({F}\right)$

### Proof

Step Hyp Ref Expression
1 tfrlem.1 ${⊢}{A}=\left\{{f}|\exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({f}Fn{x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)={F}\left({{f}↾}_{{y}}\right)\right)\right\}$
2 reluni ${⊢}\mathrm{Rel}\bigcup {A}↔\forall {g}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{Rel}{g}$
3 1 tfrlem4 ${⊢}{g}\in {A}\to \mathrm{Fun}{g}$
4 funrel ${⊢}\mathrm{Fun}{g}\to \mathrm{Rel}{g}$
5 3 4 syl ${⊢}{g}\in {A}\to \mathrm{Rel}{g}$
6 2 5 mprgbir ${⊢}\mathrm{Rel}\bigcup {A}$
7 1 recsfval ${⊢}\mathrm{recs}\left({F}\right)=\bigcup {A}$
8 7 releqi ${⊢}\mathrm{Rel}\mathrm{recs}\left({F}\right)↔\mathrm{Rel}\bigcup {A}$
9 6 8 mpbir ${⊢}\mathrm{Rel}\mathrm{recs}\left({F}\right)$