# Metamath Proof Explorer

## Theorem tfrlem8

Description: Lemma for transfinite recursion. The domain of recs is an ordinal. (Contributed by NM, 14-Aug-1994) (Proof shortened by Alan Sare, 11-Mar-2008)

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 tfrlem8 ${⊢}\mathrm{Ord}\mathrm{dom}\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 1 tfrlem3 ${⊢}{A}=\left\{{g}|\exists {z}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({g}Fn{z}\wedge \forall {w}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({w}\right)={F}\left({{g}↾}_{{w}}\right)\right)\right\}$
3 2 abeq2i ${⊢}{g}\in {A}↔\exists {z}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({g}Fn{z}\wedge \forall {w}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({w}\right)={F}\left({{g}↾}_{{w}}\right)\right)$
4 fndm ${⊢}{g}Fn{z}\to \mathrm{dom}{g}={z}$
5 4 adantr ${⊢}\left({g}Fn{z}\wedge \forall {w}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({w}\right)={F}\left({{g}↾}_{{w}}\right)\right)\to \mathrm{dom}{g}={z}$
6 5 eleq1d ${⊢}\left({g}Fn{z}\wedge \forall {w}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({w}\right)={F}\left({{g}↾}_{{w}}\right)\right)\to \left(\mathrm{dom}{g}\in \mathrm{On}↔{z}\in \mathrm{On}\right)$
7 6 biimprcd ${⊢}{z}\in \mathrm{On}\to \left(\left({g}Fn{z}\wedge \forall {w}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({w}\right)={F}\left({{g}↾}_{{w}}\right)\right)\to \mathrm{dom}{g}\in \mathrm{On}\right)$
8 7 rexlimiv ${⊢}\exists {z}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({g}Fn{z}\wedge \forall {w}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({w}\right)={F}\left({{g}↾}_{{w}}\right)\right)\to \mathrm{dom}{g}\in \mathrm{On}$
9 3 8 sylbi ${⊢}{g}\in {A}\to \mathrm{dom}{g}\in \mathrm{On}$
10 eleq1a ${⊢}\mathrm{dom}{g}\in \mathrm{On}\to \left({z}=\mathrm{dom}{g}\to {z}\in \mathrm{On}\right)$
11 9 10 syl ${⊢}{g}\in {A}\to \left({z}=\mathrm{dom}{g}\to {z}\in \mathrm{On}\right)$
12 11 rexlimiv ${⊢}\exists {g}\in {A}\phantom{\rule{.4em}{0ex}}{z}=\mathrm{dom}{g}\to {z}\in \mathrm{On}$
13 12 abssi ${⊢}\left\{{z}|\exists {g}\in {A}\phantom{\rule{.4em}{0ex}}{z}=\mathrm{dom}{g}\right\}\subseteq \mathrm{On}$
14 ssorduni ${⊢}\left\{{z}|\exists {g}\in {A}\phantom{\rule{.4em}{0ex}}{z}=\mathrm{dom}{g}\right\}\subseteq \mathrm{On}\to \mathrm{Ord}\bigcup \left\{{z}|\exists {g}\in {A}\phantom{\rule{.4em}{0ex}}{z}=\mathrm{dom}{g}\right\}$
15 13 14 ax-mp ${⊢}\mathrm{Ord}\bigcup \left\{{z}|\exists {g}\in {A}\phantom{\rule{.4em}{0ex}}{z}=\mathrm{dom}{g}\right\}$
16 1 recsfval ${⊢}\mathrm{recs}\left({F}\right)=\bigcup {A}$
17 16 dmeqi ${⊢}\mathrm{dom}\mathrm{recs}\left({F}\right)=\mathrm{dom}\bigcup {A}$
18 dmuni ${⊢}\mathrm{dom}\bigcup {A}=\bigcup _{{g}\in {A}}\mathrm{dom}{g}$
19 vex ${⊢}{g}\in \mathrm{V}$
20 19 dmex ${⊢}\mathrm{dom}{g}\in \mathrm{V}$
21 20 dfiun2 ${⊢}\bigcup _{{g}\in {A}}\mathrm{dom}{g}=\bigcup \left\{{z}|\exists {g}\in {A}\phantom{\rule{.4em}{0ex}}{z}=\mathrm{dom}{g}\right\}$
22 17 18 21 3eqtri ${⊢}\mathrm{dom}\mathrm{recs}\left({F}\right)=\bigcup \left\{{z}|\exists {g}\in {A}\phantom{\rule{.4em}{0ex}}{z}=\mathrm{dom}{g}\right\}$
23 ordeq ${⊢}\mathrm{dom}\mathrm{recs}\left({F}\right)=\bigcup \left\{{z}|\exists {g}\in {A}\phantom{\rule{.4em}{0ex}}{z}=\mathrm{dom}{g}\right\}\to \left(\mathrm{Ord}\mathrm{dom}\mathrm{recs}\left({F}\right)↔\mathrm{Ord}\bigcup \left\{{z}|\exists {g}\in {A}\phantom{\rule{.4em}{0ex}}{z}=\mathrm{dom}{g}\right\}\right)$
24 22 23 ax-mp ${⊢}\mathrm{Ord}\mathrm{dom}\mathrm{recs}\left({F}\right)↔\mathrm{Ord}\bigcup \left\{{z}|\exists {g}\in {A}\phantom{\rule{.4em}{0ex}}{z}=\mathrm{dom}{g}\right\}$
25 15 24 mpbir ${⊢}\mathrm{Ord}\mathrm{dom}\mathrm{recs}\left({F}\right)$