# Metamath Proof Explorer

## Theorem tfrlem16

Description: Lemma for finite recursion. Without assuming ax-rep , we can show that the domain of the constructed function is a limit ordinal, and hence contains all the finite ordinals. (Contributed by Mario Carneiro, 14-Nov-2014)

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 tfrlem16 ${⊢}\mathrm{Lim}\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 tfrlem8 ${⊢}\mathrm{Ord}\mathrm{dom}\mathrm{recs}\left({F}\right)$
3 ordzsl ${⊢}\mathrm{Ord}\mathrm{dom}\mathrm{recs}\left({F}\right)↔\left(\mathrm{dom}\mathrm{recs}\left({F}\right)=\varnothing \vee \exists {z}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\mathrm{dom}\mathrm{recs}\left({F}\right)=\mathrm{suc}{z}\vee \mathrm{Lim}\mathrm{dom}\mathrm{recs}\left({F}\right)\right)$
4 2 3 mpbi ${⊢}\left(\mathrm{dom}\mathrm{recs}\left({F}\right)=\varnothing \vee \exists {z}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\mathrm{dom}\mathrm{recs}\left({F}\right)=\mathrm{suc}{z}\vee \mathrm{Lim}\mathrm{dom}\mathrm{recs}\left({F}\right)\right)$
5 res0 ${⊢}{\mathrm{recs}\left({F}\right)↾}_{\varnothing }=\varnothing$
6 0ex ${⊢}\varnothing \in \mathrm{V}$
7 5 6 eqeltri ${⊢}{\mathrm{recs}\left({F}\right)↾}_{\varnothing }\in \mathrm{V}$
8 0elon ${⊢}\varnothing \in \mathrm{On}$
9 1 tfrlem15 ${⊢}\varnothing \in \mathrm{On}\to \left(\varnothing \in \mathrm{dom}\mathrm{recs}\left({F}\right)↔{\mathrm{recs}\left({F}\right)↾}_{\varnothing }\in \mathrm{V}\right)$
10 8 9 ax-mp ${⊢}\varnothing \in \mathrm{dom}\mathrm{recs}\left({F}\right)↔{\mathrm{recs}\left({F}\right)↾}_{\varnothing }\in \mathrm{V}$
11 7 10 mpbir ${⊢}\varnothing \in \mathrm{dom}\mathrm{recs}\left({F}\right)$
12 11 n0ii ${⊢}¬\mathrm{dom}\mathrm{recs}\left({F}\right)=\varnothing$
13 12 pm2.21i ${⊢}\mathrm{dom}\mathrm{recs}\left({F}\right)=\varnothing \to \mathrm{Lim}\mathrm{dom}\mathrm{recs}\left({F}\right)$
14 1 tfrlem13 ${⊢}¬\mathrm{recs}\left({F}\right)\in \mathrm{V}$
15 simpr ${⊢}\left({z}\in \mathrm{On}\wedge \mathrm{dom}\mathrm{recs}\left({F}\right)=\mathrm{suc}{z}\right)\to \mathrm{dom}\mathrm{recs}\left({F}\right)=\mathrm{suc}{z}$
16 df-suc ${⊢}\mathrm{suc}{z}={z}\cup \left\{{z}\right\}$
17 15 16 syl6eq ${⊢}\left({z}\in \mathrm{On}\wedge \mathrm{dom}\mathrm{recs}\left({F}\right)=\mathrm{suc}{z}\right)\to \mathrm{dom}\mathrm{recs}\left({F}\right)={z}\cup \left\{{z}\right\}$
18 17 reseq2d ${⊢}\left({z}\in \mathrm{On}\wedge \mathrm{dom}\mathrm{recs}\left({F}\right)=\mathrm{suc}{z}\right)\to {\mathrm{recs}\left({F}\right)↾}_{\mathrm{dom}\mathrm{recs}\left({F}\right)}={\mathrm{recs}\left({F}\right)↾}_{\left({z}\cup \left\{{z}\right\}\right)}$
19 1 tfrlem6 ${⊢}\mathrm{Rel}\mathrm{recs}\left({F}\right)$
20 resdm ${⊢}\mathrm{Rel}\mathrm{recs}\left({F}\right)\to {\mathrm{recs}\left({F}\right)↾}_{\mathrm{dom}\mathrm{recs}\left({F}\right)}=\mathrm{recs}\left({F}\right)$
21 19 20 ax-mp ${⊢}{\mathrm{recs}\left({F}\right)↾}_{\mathrm{dom}\mathrm{recs}\left({F}\right)}=\mathrm{recs}\left({F}\right)$
22 resundi ${⊢}{\mathrm{recs}\left({F}\right)↾}_{\left({z}\cup \left\{{z}\right\}\right)}=\left({\mathrm{recs}\left({F}\right)↾}_{{z}}\right)\cup \left({\mathrm{recs}\left({F}\right)↾}_{\left\{{z}\right\}}\right)$
23 18 21 22 3eqtr3g ${⊢}\left({z}\in \mathrm{On}\wedge \mathrm{dom}\mathrm{recs}\left({F}\right)=\mathrm{suc}{z}\right)\to \mathrm{recs}\left({F}\right)=\left({\mathrm{recs}\left({F}\right)↾}_{{z}}\right)\cup \left({\mathrm{recs}\left({F}\right)↾}_{\left\{{z}\right\}}\right)$
24 vex ${⊢}{z}\in \mathrm{V}$
25 24 sucid ${⊢}{z}\in \mathrm{suc}{z}$
26 25 15 eleqtrrid ${⊢}\left({z}\in \mathrm{On}\wedge \mathrm{dom}\mathrm{recs}\left({F}\right)=\mathrm{suc}{z}\right)\to {z}\in \mathrm{dom}\mathrm{recs}\left({F}\right)$
27 1 tfrlem9a ${⊢}{z}\in \mathrm{dom}\mathrm{recs}\left({F}\right)\to {\mathrm{recs}\left({F}\right)↾}_{{z}}\in \mathrm{V}$
28 26 27 syl ${⊢}\left({z}\in \mathrm{On}\wedge \mathrm{dom}\mathrm{recs}\left({F}\right)=\mathrm{suc}{z}\right)\to {\mathrm{recs}\left({F}\right)↾}_{{z}}\in \mathrm{V}$
29 snex ${⊢}\left\{⟨{z},\mathrm{recs}\left({F}\right)\left({z}\right)⟩\right\}\in \mathrm{V}$
30 1 tfrlem7 ${⊢}\mathrm{Fun}\mathrm{recs}\left({F}\right)$
31 funressn ${⊢}\mathrm{Fun}\mathrm{recs}\left({F}\right)\to {\mathrm{recs}\left({F}\right)↾}_{\left\{{z}\right\}}\subseteq \left\{⟨{z},\mathrm{recs}\left({F}\right)\left({z}\right)⟩\right\}$
32 30 31 ax-mp ${⊢}{\mathrm{recs}\left({F}\right)↾}_{\left\{{z}\right\}}\subseteq \left\{⟨{z},\mathrm{recs}\left({F}\right)\left({z}\right)⟩\right\}$
33 29 32 ssexi ${⊢}{\mathrm{recs}\left({F}\right)↾}_{\left\{{z}\right\}}\in \mathrm{V}$
34 unexg ${⊢}\left({\mathrm{recs}\left({F}\right)↾}_{{z}}\in \mathrm{V}\wedge {\mathrm{recs}\left({F}\right)↾}_{\left\{{z}\right\}}\in \mathrm{V}\right)\to \left({\mathrm{recs}\left({F}\right)↾}_{{z}}\right)\cup \left({\mathrm{recs}\left({F}\right)↾}_{\left\{{z}\right\}}\right)\in \mathrm{V}$
35 28 33 34 sylancl ${⊢}\left({z}\in \mathrm{On}\wedge \mathrm{dom}\mathrm{recs}\left({F}\right)=\mathrm{suc}{z}\right)\to \left({\mathrm{recs}\left({F}\right)↾}_{{z}}\right)\cup \left({\mathrm{recs}\left({F}\right)↾}_{\left\{{z}\right\}}\right)\in \mathrm{V}$
36 23 35 eqeltrd ${⊢}\left({z}\in \mathrm{On}\wedge \mathrm{dom}\mathrm{recs}\left({F}\right)=\mathrm{suc}{z}\right)\to \mathrm{recs}\left({F}\right)\in \mathrm{V}$
37 36 rexlimiva ${⊢}\exists {z}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\mathrm{dom}\mathrm{recs}\left({F}\right)=\mathrm{suc}{z}\to \mathrm{recs}\left({F}\right)\in \mathrm{V}$
38 14 37 mto ${⊢}¬\exists {z}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\mathrm{dom}\mathrm{recs}\left({F}\right)=\mathrm{suc}{z}$
39 38 pm2.21i ${⊢}\exists {z}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\mathrm{dom}\mathrm{recs}\left({F}\right)=\mathrm{suc}{z}\to \mathrm{Lim}\mathrm{dom}\mathrm{recs}\left({F}\right)$
40 id ${⊢}\mathrm{Lim}\mathrm{dom}\mathrm{recs}\left({F}\right)\to \mathrm{Lim}\mathrm{dom}\mathrm{recs}\left({F}\right)$
41 13 39 40 3jaoi ${⊢}\left(\mathrm{dom}\mathrm{recs}\left({F}\right)=\varnothing \vee \exists {z}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\mathrm{dom}\mathrm{recs}\left({F}\right)=\mathrm{suc}{z}\vee \mathrm{Lim}\mathrm{dom}\mathrm{recs}\left({F}\right)\right)\to \mathrm{Lim}\mathrm{dom}\mathrm{recs}\left({F}\right)$
42 4 41 ax-mp ${⊢}\mathrm{Lim}\mathrm{dom}\mathrm{recs}\left({F}\right)$