Theorem dnnumch2

Description: Define an enumeration (weak dominance version) of a set from a choice 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	dnnumch2	$$⊢\phi \to A\subseteq \mathrm{ran}F$$

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	1 2 3	dnnumch1	$$⊢\phi \to \exists x\in \mathrm{On}\left({F\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}A$$
5		f1ofo	$$⊢\left({F\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}A\to \left({F\upharpoonright }_x\right):x\underset{onto}{⟶}A$$
6		forn	$$⊢\left({F\upharpoonright }_x\right):x\underset{onto}{⟶}A\to \mathrm{ran}\left({F\upharpoonright }_x\right)=A$$
7	5 6	syl	$$⊢\left({F\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}A\to \mathrm{ran}\left({F\upharpoonright }_x\right)=A$$
8		resss	$$⊢{F\upharpoonright }_x\subseteq F$$
9		rnss	$$⊢{F\upharpoonright }_x\subseteq F\to \mathrm{ran}\left({F\upharpoonright }_x\right)\subseteq \mathrm{ran}F$$
10	8 9	mp1i	$$⊢\left({F\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}A\to \mathrm{ran}\left({F\upharpoonright }_x\right)\subseteq \mathrm{ran}F$$
11	7 10	eqsstrrd	$$⊢\left({F\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}A\to A\subseteq \mathrm{ran}F$$
12	11	a1i	$$⊢\phi \to \left(\left({F\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}A\to A\subseteq \mathrm{ran}F\right)$$
13	12	rexlimdvw	$$⊢\phi \to \left(\exists x\in \mathrm{On}\left({F\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}A\to A\subseteq \mathrm{ran}F\right)$$
14	4 13	mpd	$$⊢\phi \to A\subseteq \mathrm{ran}F$$