Theorem dnnumch3lem

Description: Value of the ordinal injection function. (Contributed by Stefan O'Rear, 18-Jan-2015)

	Ref	Expression
Hypotheses	dnnumch.f	$$⊢F=\mathrm{recs}\left(\left(z\in \mathrm{V}⟼G\left(A\setminus \mathrm{ran}z\right)\right)\right)$$
	dnnumch.a	$$⊢\phi \to A\in V$$
	dnnumch.g	$$⊢\phi \to \forall y\in 𝒫A\left(y\ne \varnothing \to G\left(y\right)\in y\right)$$
Assertion	dnnumch3lem	$$⊢\left(\phi \wedge w\in A\right)\to \left(x\in A⟼\bigcap F^{-1}\left[\left\{x\right\}\right]\right)\left(w\right)=\bigcap F^{-1}\left[\left\{w\right\}\right]$$

Proof

Step	Hyp	Ref	Expression
1		dnnumch.f	$$⊢F=\mathrm{recs}\left(\left(z\in \mathrm{V}⟼G\left(A\setminus \mathrm{ran}z\right)\right)\right)$$
2		dnnumch.a	$$⊢\phi \to A\in V$$
3		dnnumch.g	$$⊢\phi \to \forall y\in 𝒫A\left(y\ne \varnothing \to G\left(y\right)\in y\right)$$
4		eqid	$$⊢\left(x\in A⟼\bigcap F^{-1}\left[\left\{x\right\}\right]\right)=\left(x\in A⟼\bigcap F^{-1}\left[\left\{x\right\}\right]\right)$$
5		sneq	$$⊢x=w\to \left\{x\right\}=\left\{w\right\}$$
6	5	imaeq2d	$$⊢x=w\to F^{-1}\left[\left\{x\right\}\right]=F^{-1}\left[\left\{w\right\}\right]$$
7	6	inteqd	$$⊢x=w\to \bigcap F^{-1}\left[\left\{x\right\}\right]=\bigcap F^{-1}\left[\left\{w\right\}\right]$$
8		simpr	$$⊢\left(\phi \wedge w\in A\right)\to w\in A$$
9		cnvimass	$$⊢F^{-1}\left[\left\{w\right\}\right]\subseteq \mathrm{dom}F$$
10	1	tfr1	$$⊢FFn\mathrm{On}$$
11	10	fndmi	$$⊢\mathrm{dom}F=\mathrm{On}$$
12	9 11	sseqtri	$$⊢F^{-1}\left[\left\{w\right\}\right]\subseteq \mathrm{On}$$
13	1 2 3	dnnumch2	$$⊢\phi \to A\subseteq \mathrm{ran}F$$
14	13	sselda	$$⊢\left(\phi \wedge w\in A\right)\to w\in \mathrm{ran}F$$
15		inisegn0	$$⊢w\in \mathrm{ran}F\leftrightarrow F^{-1}\left[\left\{w\right\}\right]\ne \varnothing$$
16	14 15	sylib	$$⊢\left(\phi \wedge w\in A\right)\to F^{-1}\left[\left\{w\right\}\right]\ne \varnothing$$
17		oninton	$$⊢\left(F^{-1}\left[\left\{w\right\}\right]\subseteq \mathrm{On}\wedge F^{-1}\left[\left\{w\right\}\right]\ne \varnothing \right)\to \bigcap F^{-1}\left[\left\{w\right\}\right]\in \mathrm{On}$$
18	12 16 17	sylancr	$$⊢\left(\phi \wedge w\in A\right)\to \bigcap F^{-1}\left[\left\{w\right\}\right]\in \mathrm{On}$$
19	4 7 8 18	fvmptd3	$$⊢\left(\phi \wedge w\in A\right)\to \left(x\in A⟼\bigcap F^{-1}\left[\left\{x\right\}\right]\right)\left(w\right)=\bigcap F^{-1}\left[\left\{w\right\}\right]$$