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}\left(fFnx\wedge \forall y\in xf\left(y\right)=F\left({f\upharpoonright }_y\right)\right)\right\}$$
Assertion	tfrlem13	$$⊢\neg \mathrm{recs}\left(F\right)\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		tfrlem.1	$$⊢A=\left\{f|\exists x\in \mathrm{On}\left(fFnx\wedge \forall y\in xf\left(y\right)=F\left({f\upharpoonright }_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 \neg \mathrm{dom}\mathrm{recs}\left(F\right)\in \mathrm{dom}\mathrm{recs}\left(F\right)$$
4	2 3	ax-mp	$$⊢\neg \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}\leftrightarrow \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	$$⊢\neg \mathrm{recs}\left(F\right)\in \mathrm{V}$$