Theorem dnnumch1

Description: Define an enumeration of a set from a choice function; second part, it restricts to a bijection.EDITORIAL: overlaps dfac8a . (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	dnnumch1	$$⊢\phi \to \exists x\in \mathrm{On}\left({F\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}A$$

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		recsval	$$⊢x\in \mathrm{On}\to \mathrm{recs}\left(\left(z\in \mathrm{V}⟼G\left(A\setminus \mathrm{ran}z\right)\right)\right)\left(x\right)=\left(z\in \mathrm{V}⟼G\left(A\setminus \mathrm{ran}z\right)\right)\left({\mathrm{recs}\left(\left(z\in \mathrm{V}⟼G\left(A\setminus \mathrm{ran}z\right)\right)\right)\upharpoonright }_x\right)$$
5	1	fveq1i	$$⊢F\left(x\right)=\mathrm{recs}\left(\left(z\in \mathrm{V}⟼G\left(A\setminus \mathrm{ran}z\right)\right)\right)\left(x\right)$$
6	1	tfr1	$$⊢FFn\mathrm{On}$$
7		fnfun	$$⊢FFn\mathrm{On}\to \mathrm{Fun}F$$
8	6 7	ax-mp	$$⊢\mathrm{Fun}F$$
9		vex	$$⊢x\in \mathrm{V}$$
10		resfunexg	$$⊢\left(\mathrm{Fun}F\wedge x\in \mathrm{V}\right)\to {F\upharpoonright }_x\in \mathrm{V}$$
11	8 9 10	mp2an	$$⊢{F\upharpoonright }_x\in \mathrm{V}$$
12		rneq	$$⊢w={F\upharpoonright }_x\to \mathrm{ran}w=\mathrm{ran}\left({F\upharpoonright }_x\right)$$
13		df-ima	$$⊢F\left[x\right]=\mathrm{ran}\left({F\upharpoonright }_x\right)$$
14	12 13	syl6eqr	$$⊢w={F\upharpoonright }_x\to \mathrm{ran}w=F\left[x\right]$$
15	14	difeq2d	$$⊢w={F\upharpoonright }_x\to A\setminus \mathrm{ran}w=A\setminus F\left[x\right]$$
16	15	fveq2d	$$⊢w={F\upharpoonright }_x\to G\left(A\setminus \mathrm{ran}w\right)=G\left(A\setminus F\left[x\right]\right)$$
17		rneq	$$⊢z=w\to \mathrm{ran}z=\mathrm{ran}w$$
18	17	difeq2d	$$⊢z=w\to A\setminus \mathrm{ran}z=A\setminus \mathrm{ran}w$$
19	18	fveq2d	$$⊢z=w\to G\left(A\setminus \mathrm{ran}z\right)=G\left(A\setminus \mathrm{ran}w\right)$$
20	19	cbvmptv	$$⊢\left(z\in \mathrm{V}⟼G\left(A\setminus \mathrm{ran}z\right)\right)=\left(w\in \mathrm{V}⟼G\left(A\setminus \mathrm{ran}w\right)\right)$$
21		fvex	$$⊢G\left(A\setminus F\left[x\right]\right)\in \mathrm{V}$$
22	16 20 21	fvmpt	$$⊢{F\upharpoonright }_x\in \mathrm{V}\to \left(z\in \mathrm{V}⟼G\left(A\setminus \mathrm{ran}z\right)\right)\left({F\upharpoonright }_x\right)=G\left(A\setminus F\left[x\right]\right)$$
23	11 22	ax-mp	$$⊢\left(z\in \mathrm{V}⟼G\left(A\setminus \mathrm{ran}z\right)\right)\left({F\upharpoonright }_x\right)=G\left(A\setminus F\left[x\right]\right)$$
24	1	reseq1i	$$⊢{F\upharpoonright }_x={\mathrm{recs}\left(\left(z\in \mathrm{V}⟼G\left(A\setminus \mathrm{ran}z\right)\right)\right)\upharpoonright }_x$$
25	24	fveq2i	$$⊢\left(z\in \mathrm{V}⟼G\left(A\setminus \mathrm{ran}z\right)\right)\left({F\upharpoonright }_x\right)=\left(z\in \mathrm{V}⟼G\left(A\setminus \mathrm{ran}z\right)\right)\left({\mathrm{recs}\left(\left(z\in \mathrm{V}⟼G\left(A\setminus \mathrm{ran}z\right)\right)\right)\upharpoonright }_x\right)$$
26	23 25	eqtr3i	$$⊢G\left(A\setminus F\left[x\right]\right)=\left(z\in \mathrm{V}⟼G\left(A\setminus \mathrm{ran}z\right)\right)\left({\mathrm{recs}\left(\left(z\in \mathrm{V}⟼G\left(A\setminus \mathrm{ran}z\right)\right)\right)\upharpoonright }_x\right)$$
27	4 5 26	3eqtr4g	$$⊢x\in \mathrm{On}\to F\left(x\right)=G\left(A\setminus F\left[x\right]\right)$$
28	27	ad2antlr	$$⊢\left(\left(\phi \wedge x\in \mathrm{On}\right)\wedge A\setminus F\left[x\right]\ne \varnothing \right)\to F\left(x\right)=G\left(A\setminus F\left[x\right]\right)$$
29		difss	$$⊢A\setminus F\left[x\right]\subseteq A$$
30		elpw2g	$$⊢A\in V\to \left(A\setminus F\left[x\right]\in 𝒫A\leftrightarrow A\setminus F\left[x\right]\subseteq A\right)$$
31	2 30	syl	$$⊢\phi \to \left(A\setminus F\left[x\right]\in 𝒫A\leftrightarrow A\setminus F\left[x\right]\subseteq A\right)$$
32	29 31	mpbiri	$$⊢\phi \to A\setminus F\left[x\right]\in 𝒫A$$
33		neeq1	$$⊢y=A\setminus F\left[x\right]\to \left(y\ne \varnothing \leftrightarrow A\setminus F\left[x\right]\ne \varnothing \right)$$
34		fveq2	$$⊢y=A\setminus F\left[x\right]\to G\left(y\right)=G\left(A\setminus F\left[x\right]\right)$$
35		id	$$⊢y=A\setminus F\left[x\right]\to y=A\setminus F\left[x\right]$$
36	34 35	eleq12d	$$⊢y=A\setminus F\left[x\right]\to \left(G\left(y\right)\in y\leftrightarrow G\left(A\setminus F\left[x\right]\right)\in \left(A\setminus F\left[x\right]\right)\right)$$
37	33 36	imbi12d	$$⊢y=A\setminus F\left[x\right]\to \left(\left(y\ne \varnothing \to G\left(y\right)\in y\right)\leftrightarrow \left(A\setminus F\left[x\right]\ne \varnothing \to G\left(A\setminus F\left[x\right]\right)\in \left(A\setminus F\left[x\right]\right)\right)\right)$$
38	37	rspcva	$$⊢\left(A\setminus F\left[x\right]\in 𝒫A\wedge \forall y\in 𝒫A\left(y\ne \varnothing \to G\left(y\right)\in y\right)\right)\to \left(A\setminus F\left[x\right]\ne \varnothing \to G\left(A\setminus F\left[x\right]\right)\in \left(A\setminus F\left[x\right]\right)\right)$$
39	32 3 38	syl2anc	$$⊢\phi \to \left(A\setminus F\left[x\right]\ne \varnothing \to G\left(A\setminus F\left[x\right]\right)\in \left(A\setminus F\left[x\right]\right)\right)$$
40	39	adantr	$$⊢\left(\phi \wedge x\in \mathrm{On}\right)\to \left(A\setminus F\left[x\right]\ne \varnothing \to G\left(A\setminus F\left[x\right]\right)\in \left(A\setminus F\left[x\right]\right)\right)$$
41	40	imp	$$⊢\left(\left(\phi \wedge x\in \mathrm{On}\right)\wedge A\setminus F\left[x\right]\ne \varnothing \right)\to G\left(A\setminus F\left[x\right]\right)\in \left(A\setminus F\left[x\right]\right)$$
42	28 41	eqeltrd	$$⊢\left(\left(\phi \wedge x\in \mathrm{On}\right)\wedge A\setminus F\left[x\right]\ne \varnothing \right)\to F\left(x\right)\in \left(A\setminus F\left[x\right]\right)$$
43	42	ex	$$⊢\left(\phi \wedge x\in \mathrm{On}\right)\to \left(A\setminus F\left[x\right]\ne \varnothing \to F\left(x\right)\in \left(A\setminus F\left[x\right]\right)\right)$$
44	43	ralrimiva	$$⊢\phi \to \forall x\in \mathrm{On}\left(A\setminus F\left[x\right]\ne \varnothing \to F\left(x\right)\in \left(A\setminus F\left[x\right]\right)\right)$$
45	6	tz7.49c	$$⊢\left(A\in V\wedge \forall x\in \mathrm{On}\left(A\setminus F\left[x\right]\ne \varnothing \to F\left(x\right)\in \left(A\setminus F\left[x\right]\right)\right)\right)\to \exists x\in \mathrm{On}\left({F\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}A$$
46	2 44 45	syl2anc	$$⊢\phi \to \exists x\in \mathrm{On}\left({F\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}A$$