Metamath Proof Explorer

Theorem tfrlem14

Description: Lemma for transfinite recursion. Assuming ax-rep , dom recs e.V <-> recs e. V , so since dom recs is an ordinal, it must be equal to On . (Contributed by NM, 14-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 tfrlem14 ${⊢}\mathrm{dom}\mathrm{recs}\left({F}\right)=\mathrm{On}$

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 tfrlem13 ${⊢}¬\mathrm{recs}\left({F}\right)\in \mathrm{V}$
3 1 tfrlem7 ${⊢}\mathrm{Fun}\mathrm{recs}\left({F}\right)$
4 funex ${⊢}\left(\mathrm{Fun}\mathrm{recs}\left({F}\right)\wedge \mathrm{dom}\mathrm{recs}\left({F}\right)\in \mathrm{On}\right)\to \mathrm{recs}\left({F}\right)\in \mathrm{V}$
5 3 4 mpan ${⊢}\mathrm{dom}\mathrm{recs}\left({F}\right)\in \mathrm{On}\to \mathrm{recs}\left({F}\right)\in \mathrm{V}$
6 2 5 mto ${⊢}¬\mathrm{dom}\mathrm{recs}\left({F}\right)\in \mathrm{On}$
7 1 tfrlem8 ${⊢}\mathrm{Ord}\mathrm{dom}\mathrm{recs}\left({F}\right)$
8 ordeleqon ${⊢}\mathrm{Ord}\mathrm{dom}\mathrm{recs}\left({F}\right)↔\left(\mathrm{dom}\mathrm{recs}\left({F}\right)\in \mathrm{On}\vee \mathrm{dom}\mathrm{recs}\left({F}\right)=\mathrm{On}\right)$
9 7 8 mpbi ${⊢}\left(\mathrm{dom}\mathrm{recs}\left({F}\right)\in \mathrm{On}\vee \mathrm{dom}\mathrm{recs}\left({F}\right)=\mathrm{On}\right)$
10 6 9 mtpor ${⊢}\mathrm{dom}\mathrm{recs}\left({F}\right)=\mathrm{On}$