# Metamath Proof Explorer

## Theorem tfrlem13

Description: Lemma for transfinite recursion. If recs is a set function, then C is acceptable, and thus a subset of recs , but dom C is bigger than dom recs . This is a contradiction, so recs must be a proper class function. (Contributed by NM, 14-Aug-1994) (Revised 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 tfrlem13 ${⊢}¬\mathrm{recs}\left({F}\right)\in \mathrm{V}$

### 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 ordirr ${⊢}\mathrm{Ord}\mathrm{dom}\mathrm{recs}\left({F}\right)\to ¬\mathrm{dom}\mathrm{recs}\left({F}\right)\in \mathrm{dom}\mathrm{recs}\left({F}\right)$
4 2 3 ax-mp ${⊢}¬\mathrm{dom}\mathrm{recs}\left({F}\right)\in \mathrm{dom}\mathrm{recs}\left({F}\right)$
5 eqid ${⊢}\mathrm{recs}\left({F}\right)\cup \left\{⟨\mathrm{dom}\mathrm{recs}\left({F}\right),{F}\left(\mathrm{recs}\left({F}\right)\right)⟩\right\}=\mathrm{recs}\left({F}\right)\cup \left\{⟨\mathrm{dom}\mathrm{recs}\left({F}\right),{F}\left(\mathrm{recs}\left({F}\right)\right)⟩\right\}$
6 1 5 tfrlem12 ${⊢}\mathrm{recs}\left({F}\right)\in \mathrm{V}\to \mathrm{recs}\left({F}\right)\cup \left\{⟨\mathrm{dom}\mathrm{recs}\left({F}\right),{F}\left(\mathrm{recs}\left({F}\right)\right)⟩\right\}\in {A}$
7 elssuni ${⊢}\mathrm{recs}\left({F}\right)\cup \left\{⟨\mathrm{dom}\mathrm{recs}\left({F}\right),{F}\left(\mathrm{recs}\left({F}\right)\right)⟩\right\}\in {A}\to \mathrm{recs}\left({F}\right)\cup \left\{⟨\mathrm{dom}\mathrm{recs}\left({F}\right),{F}\left(\mathrm{recs}\left({F}\right)\right)⟩\right\}\subseteq \bigcup {A}$
8 1 recsfval ${⊢}\mathrm{recs}\left({F}\right)=\bigcup {A}$
9 7 8 sseqtrrdi ${⊢}\mathrm{recs}\left({F}\right)\cup \left\{⟨\mathrm{dom}\mathrm{recs}\left({F}\right),{F}\left(\mathrm{recs}\left({F}\right)\right)⟩\right\}\in {A}\to \mathrm{recs}\left({F}\right)\cup \left\{⟨\mathrm{dom}\mathrm{recs}\left({F}\right),{F}\left(\mathrm{recs}\left({F}\right)\right)⟩\right\}\subseteq \mathrm{recs}\left({F}\right)$
10 dmss ${⊢}\mathrm{recs}\left({F}\right)\cup \left\{⟨\mathrm{dom}\mathrm{recs}\left({F}\right),{F}\left(\mathrm{recs}\left({F}\right)\right)⟩\right\}\subseteq \mathrm{recs}\left({F}\right)\to \mathrm{dom}\left(\mathrm{recs}\left({F}\right)\cup \left\{⟨\mathrm{dom}\mathrm{recs}\left({F}\right),{F}\left(\mathrm{recs}\left({F}\right)\right)⟩\right\}\right)\subseteq \mathrm{dom}\mathrm{recs}\left({F}\right)$
11 6 9 10 3syl ${⊢}\mathrm{recs}\left({F}\right)\in \mathrm{V}\to \mathrm{dom}\left(\mathrm{recs}\left({F}\right)\cup \left\{⟨\mathrm{dom}\mathrm{recs}\left({F}\right),{F}\left(\mathrm{recs}\left({F}\right)\right)⟩\right\}\right)\subseteq \mathrm{dom}\mathrm{recs}\left({F}\right)$
12 2 a1i ${⊢}\mathrm{recs}\left({F}\right)\in \mathrm{V}\to \mathrm{Ord}\mathrm{dom}\mathrm{recs}\left({F}\right)$
13 dmexg ${⊢}\mathrm{recs}\left({F}\right)\in \mathrm{V}\to \mathrm{dom}\mathrm{recs}\left({F}\right)\in \mathrm{V}$
14 elon2 ${⊢}\mathrm{dom}\mathrm{recs}\left({F}\right)\in \mathrm{On}↔\left(\mathrm{Ord}\mathrm{dom}\mathrm{recs}\left({F}\right)\wedge \mathrm{dom}\mathrm{recs}\left({F}\right)\in \mathrm{V}\right)$
15 12 13 14 sylanbrc ${⊢}\mathrm{recs}\left({F}\right)\in \mathrm{V}\to \mathrm{dom}\mathrm{recs}\left({F}\right)\in \mathrm{On}$
16 sucidg ${⊢}\mathrm{dom}\mathrm{recs}\left({F}\right)\in \mathrm{On}\to \mathrm{dom}\mathrm{recs}\left({F}\right)\in \mathrm{suc}\mathrm{dom}\mathrm{recs}\left({F}\right)$
17 15 16 syl ${⊢}\mathrm{recs}\left({F}\right)\in \mathrm{V}\to \mathrm{dom}\mathrm{recs}\left({F}\right)\in \mathrm{suc}\mathrm{dom}\mathrm{recs}\left({F}\right)$
18 1 5 tfrlem10 ${⊢}\mathrm{dom}\mathrm{recs}\left({F}\right)\in \mathrm{On}\to \left(\mathrm{recs}\left({F}\right)\cup \left\{⟨\mathrm{dom}\mathrm{recs}\left({F}\right),{F}\left(\mathrm{recs}\left({F}\right)\right)⟩\right\}\right)Fn\mathrm{suc}\mathrm{dom}\mathrm{recs}\left({F}\right)$
19 fndm ${⊢}\left(\mathrm{recs}\left({F}\right)\cup \left\{⟨\mathrm{dom}\mathrm{recs}\left({F}\right),{F}\left(\mathrm{recs}\left({F}\right)\right)⟩\right\}\right)Fn\mathrm{suc}\mathrm{dom}\mathrm{recs}\left({F}\right)\to \mathrm{dom}\left(\mathrm{recs}\left({F}\right)\cup \left\{⟨\mathrm{dom}\mathrm{recs}\left({F}\right),{F}\left(\mathrm{recs}\left({F}\right)\right)⟩\right\}\right)=\mathrm{suc}\mathrm{dom}\mathrm{recs}\left({F}\right)$
20 15 18 19 3syl ${⊢}\mathrm{recs}\left({F}\right)\in \mathrm{V}\to \mathrm{dom}\left(\mathrm{recs}\left({F}\right)\cup \left\{⟨\mathrm{dom}\mathrm{recs}\left({F}\right),{F}\left(\mathrm{recs}\left({F}\right)\right)⟩\right\}\right)=\mathrm{suc}\mathrm{dom}\mathrm{recs}\left({F}\right)$
21 17 20 eleqtrrd ${⊢}\mathrm{recs}\left({F}\right)\in \mathrm{V}\to \mathrm{dom}\mathrm{recs}\left({F}\right)\in \mathrm{dom}\left(\mathrm{recs}\left({F}\right)\cup \left\{⟨\mathrm{dom}\mathrm{recs}\left({F}\right),{F}\left(\mathrm{recs}\left({F}\right)\right)⟩\right\}\right)$
22 11 21 sseldd ${⊢}\mathrm{recs}\left({F}\right)\in \mathrm{V}\to \mathrm{dom}\mathrm{recs}\left({F}\right)\in \mathrm{dom}\mathrm{recs}\left({F}\right)$
23 4 22 mto ${⊢}¬\mathrm{recs}\left({F}\right)\in \mathrm{V}$