Theorem tfrlem10

Description: Lemma for transfinite recursion. We define class C by extending recs with one ordered pair. We will assume, falsely, that domain of recs is a member of, and thus not equal to, On . Using this assumption we will prove facts about C that will lead to a contradiction in tfrlem14 , thus showing the domain of recs does in fact equal On . Here we show (under the false assumption) that C is a function extending the domain of recs ( F ) by one. (Contributed by NM, 14-Aug-1994) (Revised by Mario Carneiro, 9-May-2015)

	Ref	Expression
Hypotheses	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\}$$
	tfrlem.3	$$⊢C=\mathrm{recs}\left(F\right)\cup \left\{⟨\mathrm{dom}\mathrm{recs}\left(F\right),F\left(\mathrm{recs}\left(F\right)\right)⟩\right\}$$
Assertion	tfrlem10	$$⊢\mathrm{dom}\mathrm{recs}\left(F\right)\in \mathrm{On}\to CFn\mathrm{suc}\mathrm{dom}\mathrm{recs}\left(F\right)$$

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		tfrlem.3	$$⊢C=\mathrm{recs}\left(F\right)\cup \left\{⟨\mathrm{dom}\mathrm{recs}\left(F\right),F\left(\mathrm{recs}\left(F\right)\right)⟩\right\}$$
3		fvex	$$⊢F\left(\mathrm{recs}\left(F\right)\right)\in \mathrm{V}$$
4		funsng	$$⊢\left(\mathrm{dom}\mathrm{recs}\left(F\right)\in \mathrm{On}\wedge F\left(\mathrm{recs}\left(F\right)\right)\in \mathrm{V}\right)\to \mathrm{Fun}\left\{⟨\mathrm{dom}\mathrm{recs}\left(F\right),F\left(\mathrm{recs}\left(F\right)\right)⟩\right\}$$
5	3 4	mpan2	$$⊢\mathrm{dom}\mathrm{recs}\left(F\right)\in \mathrm{On}\to \mathrm{Fun}\left\{⟨\mathrm{dom}\mathrm{recs}\left(F\right),F\left(\mathrm{recs}\left(F\right)\right)⟩\right\}$$
6	1	tfrlem7	$$⊢\mathrm{Fun}\mathrm{recs}\left(F\right)$$
7	5 6	jctil	$$⊢\mathrm{dom}\mathrm{recs}\left(F\right)\in \mathrm{On}\to \left(\mathrm{Fun}\mathrm{recs}\left(F\right)\wedge \mathrm{Fun}\left\{⟨\mathrm{dom}\mathrm{recs}\left(F\right),F\left(\mathrm{recs}\left(F\right)\right)⟩\right\}\right)$$
8	3	dmsnop	$$⊢\mathrm{dom}\left\{⟨\mathrm{dom}\mathrm{recs}\left(F\right),F\left(\mathrm{recs}\left(F\right)\right)⟩\right\}=\left\{\mathrm{dom}\mathrm{recs}\left(F\right)\right\}$$
9	8	ineq2i	$$⊢\mathrm{dom}\mathrm{recs}\left(F\right)\cap \mathrm{dom}\left\{⟨\mathrm{dom}\mathrm{recs}\left(F\right),F\left(\mathrm{recs}\left(F\right)\right)⟩\right\}=\mathrm{dom}\mathrm{recs}\left(F\right)\cap \left\{\mathrm{dom}\mathrm{recs}\left(F\right)\right\}$$
10	1	tfrlem8	$$⊢\mathrm{Ord}\mathrm{dom}\mathrm{recs}\left(F\right)$$
11		orddisj	$$⊢\mathrm{Ord}\mathrm{dom}\mathrm{recs}\left(F\right)\to \mathrm{dom}\mathrm{recs}\left(F\right)\cap \left\{\mathrm{dom}\mathrm{recs}\left(F\right)\right\}=\varnothing$$
12	10 11	ax-mp	$$⊢\mathrm{dom}\mathrm{recs}\left(F\right)\cap \left\{\mathrm{dom}\mathrm{recs}\left(F\right)\right\}=\varnothing$$
13	9 12	eqtri	$$⊢\mathrm{dom}\mathrm{recs}\left(F\right)\cap \mathrm{dom}\left\{⟨\mathrm{dom}\mathrm{recs}\left(F\right),F\left(\mathrm{recs}\left(F\right)\right)⟩\right\}=\varnothing$$
14		funun	$$⊢\left(\left(\mathrm{Fun}\mathrm{recs}\left(F\right)\wedge \mathrm{Fun}\left\{⟨\mathrm{dom}\mathrm{recs}\left(F\right),F\left(\mathrm{recs}\left(F\right)\right)⟩\right\}\right)\wedge \mathrm{dom}\mathrm{recs}\left(F\right)\cap \mathrm{dom}\left\{⟨\mathrm{dom}\mathrm{recs}\left(F\right),F\left(\mathrm{recs}\left(F\right)\right)⟩\right\}=\varnothing \right)\to \mathrm{Fun}\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)$$
15	7 13 14	sylancl	$$⊢\mathrm{dom}\mathrm{recs}\left(F\right)\in \mathrm{On}\to \mathrm{Fun}\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)$$
16	8	uneq2i	$$⊢\mathrm{dom}\mathrm{recs}\left(F\right)\cup \mathrm{dom}\left\{⟨\mathrm{dom}\mathrm{recs}\left(F\right),F\left(\mathrm{recs}\left(F\right)\right)⟩\right\}=\mathrm{dom}\mathrm{recs}\left(F\right)\cup \left\{\mathrm{dom}\mathrm{recs}\left(F\right)\right\}$$
17		dmun	$$⊢\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{dom}\mathrm{recs}\left(F\right)\cup \mathrm{dom}\left\{⟨\mathrm{dom}\mathrm{recs}\left(F\right),F\left(\mathrm{recs}\left(F\right)\right)⟩\right\}$$
18		df-suc	$$⊢\mathrm{suc}\mathrm{dom}\mathrm{recs}\left(F\right)=\mathrm{dom}\mathrm{recs}\left(F\right)\cup \left\{\mathrm{dom}\mathrm{recs}\left(F\right)\right\}$$
19	16 17 18	3eqtr4i	$$⊢\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		df-fn	$$⊢\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)\leftrightarrow \left(\mathrm{Fun}\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)\wedge \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)\right)$$
21	15 19 20	sylanblrc	$$⊢\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)$$
22	2	fneq1i	$$⊢CFn\mathrm{suc}\mathrm{dom}\mathrm{recs}\left(F\right)\leftrightarrow \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)$$
23	21 22	sylibr	$$⊢\mathrm{dom}\mathrm{recs}\left(F\right)\in \mathrm{On}\to CFn\mathrm{suc}\mathrm{dom}\mathrm{recs}\left(F\right)$$