Theorem wfrlem13

Description: Lemma for well-ordered recursion. From here through wfrlem16 , we aim to prove that dom F = A . We do this by supposing that there is an element z of A that is not in dom F . We then define C by extending dom F with the appropriate value at z . We then show that z cannot be an R minimal element of ( A \ dom F ) , meaning that ( A \ dom F ) must be empty, so dom F = A . Here, we show that C is a function extending the domain of F by one. (Contributed by Scott Fenton, 21-Apr-2011) (Revised by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Hypotheses	wfrlem13.1	$$⊢R\mathrm{We}A$$
	wfrlem13.2	$$⊢R\mathrm{Se}A$$
	wfrlem13.3	$$⊢F=\mathrm{wrecs}\left(R,A,G\right)$$
	wfrlem13.4	$$⊢C=F\cup \left\{⟨z,G\left({F\upharpoonright }_{Pred\left(R,A,z\right)}\right)⟩\right\}$$
Assertion	wfrlem13	$$⊢z\in \left(A\setminus \mathrm{dom}F\right)\to CFn\left(\mathrm{dom}F\cup \left\{z\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		wfrlem13.1	$$⊢R\mathrm{We}A$$
2		wfrlem13.2	$$⊢R\mathrm{Se}A$$
3		wfrlem13.3	$$⊢F=\mathrm{wrecs}\left(R,A,G\right)$$
4		wfrlem13.4	$$⊢C=F\cup \left\{⟨z,G\left({F\upharpoonright }_{Pred\left(R,A,z\right)}\right)⟩\right\}$$
5	1 2 3	wfrfun	$$⊢\mathrm{Fun}F$$
6		vex	$$⊢z\in \mathrm{V}$$
7		fvex	$$⊢G\left({F\upharpoonright }_{Pred\left(R,A,z\right)}\right)\in \mathrm{V}$$
8	6 7	funsn	$$⊢\mathrm{Fun}\left\{⟨z,G\left({F\upharpoonright }_{Pred\left(R,A,z\right)}\right)⟩\right\}$$
9	5 8	pm3.2i	$$⊢\left(\mathrm{Fun}F\wedge \mathrm{Fun}\left\{⟨z,G\left({F\upharpoonright }_{Pred\left(R,A,z\right)}\right)⟩\right\}\right)$$
10	7	dmsnop	$$⊢\mathrm{dom}\left\{⟨z,G\left({F\upharpoonright }_{Pred\left(R,A,z\right)}\right)⟩\right\}=\left\{z\right\}$$
11	10	ineq2i	$$⊢\mathrm{dom}F\cap \mathrm{dom}\left\{⟨z,G\left({F\upharpoonright }_{Pred\left(R,A,z\right)}\right)⟩\right\}=\mathrm{dom}F\cap \left\{z\right\}$$
12		eldifn	$$⊢z\in \left(A\setminus \mathrm{dom}F\right)\to \neg z\in \mathrm{dom}F$$
13		disjsn	$$⊢\mathrm{dom}F\cap \left\{z\right\}=\varnothing \leftrightarrow \neg z\in \mathrm{dom}F$$
14	12 13	sylibr	$$⊢z\in \left(A\setminus \mathrm{dom}F\right)\to \mathrm{dom}F\cap \left\{z\right\}=\varnothing$$
15	11 14	eqtrid	$$⊢z\in \left(A\setminus \mathrm{dom}F\right)\to \mathrm{dom}F\cap \mathrm{dom}\left\{⟨z,G\left({F\upharpoonright }_{Pred\left(R,A,z\right)}\right)⟩\right\}=\varnothing$$
16		funun	$$⊢\left(\left(\mathrm{Fun}F\wedge \mathrm{Fun}\left\{⟨z,G\left({F\upharpoonright }_{Pred\left(R,A,z\right)}\right)⟩\right\}\right)\wedge \mathrm{dom}F\cap \mathrm{dom}\left\{⟨z,G\left({F\upharpoonright }_{Pred\left(R,A,z\right)}\right)⟩\right\}=\varnothing \right)\to \mathrm{Fun}\left(F\cup \left\{⟨z,G\left({F\upharpoonright }_{Pred\left(R,A,z\right)}\right)⟩\right\}\right)$$
17	9 15 16	sylancr	$$⊢z\in \left(A\setminus \mathrm{dom}F\right)\to \mathrm{Fun}\left(F\cup \left\{⟨z,G\left({F\upharpoonright }_{Pred\left(R,A,z\right)}\right)⟩\right\}\right)$$
18		dmun	$$⊢\mathrm{dom}\left(F\cup \left\{⟨z,G\left({F\upharpoonright }_{Pred\left(R,A,z\right)}\right)⟩\right\}\right)=\mathrm{dom}F\cup \mathrm{dom}\left\{⟨z,G\left({F\upharpoonright }_{Pred\left(R,A,z\right)}\right)⟩\right\}$$
19	10	uneq2i	$$⊢\mathrm{dom}F\cup \mathrm{dom}\left\{⟨z,G\left({F\upharpoonright }_{Pred\left(R,A,z\right)}\right)⟩\right\}=\mathrm{dom}F\cup \left\{z\right\}$$
20	18 19	eqtri	$$⊢\mathrm{dom}\left(F\cup \left\{⟨z,G\left({F\upharpoonright }_{Pred\left(R,A,z\right)}\right)⟩\right\}\right)=\mathrm{dom}F\cup \left\{z\right\}$$
21	4	fneq1i	$$⊢CFn\left(\mathrm{dom}F\cup \left\{z\right\}\right)\leftrightarrow \left(F\cup \left\{⟨z,G\left({F\upharpoonright }_{Pred\left(R,A,z\right)}\right)⟩\right\}\right)Fn\left(\mathrm{dom}F\cup \left\{z\right\}\right)$$
22		df-fn	$$⊢\left(F\cup \left\{⟨z,G\left({F\upharpoonright }_{Pred\left(R,A,z\right)}\right)⟩\right\}\right)Fn\left(\mathrm{dom}F\cup \left\{z\right\}\right)\leftrightarrow \left(\mathrm{Fun}\left(F\cup \left\{⟨z,G\left({F\upharpoonright }_{Pred\left(R,A,z\right)}\right)⟩\right\}\right)\wedge \mathrm{dom}\left(F\cup \left\{⟨z,G\left({F\upharpoonright }_{Pred\left(R,A,z\right)}\right)⟩\right\}\right)=\mathrm{dom}F\cup \left\{z\right\}\right)$$
23	21 22	bitri	$$⊢CFn\left(\mathrm{dom}F\cup \left\{z\right\}\right)\leftrightarrow \left(\mathrm{Fun}\left(F\cup \left\{⟨z,G\left({F\upharpoonright }_{Pred\left(R,A,z\right)}\right)⟩\right\}\right)\wedge \mathrm{dom}\left(F\cup \left\{⟨z,G\left({F\upharpoonright }_{Pred\left(R,A,z\right)}\right)⟩\right\}\right)=\mathrm{dom}F\cup \left\{z\right\}\right)$$
24	17 20 23	sylanblrc	$$⊢z\in \left(A\setminus \mathrm{dom}F\right)\to CFn\left(\mathrm{dom}F\cup \left\{z\right\}\right)$$