Theorem dfac8alem

Description: Lemma for dfac8a . If the power set of a set has a choice function, then the set is numerable. (Contributed by NM, 10-Feb-1997) (Revised by Mario Carneiro, 5-Jan-2013)

	Ref	Expression
Hypotheses	dfac8alem.2	$$⊢F=\mathrm{recs}\left(G\right)$$
	dfac8alem.3	$$⊢G=\left(f\in \mathrm{V}⟼g\left(A\setminus \mathrm{ran}f\right)\right)$$
Assertion	dfac8alem	$$⊢A\in C\to \left(\exists g\forall y\in 𝒫A\left(y\ne \varnothing \to g\left(y\right)\in y\right)\to A\in \mathrm{dom}\mathrm{card}\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfac8alem.2	$$⊢F=\mathrm{recs}\left(G\right)$$
2		dfac8alem.3	$$⊢G=\left(f\in \mathrm{V}⟼g\left(A\setminus \mathrm{ran}f\right)\right)$$
3		elex	$$⊢A\in C\to A\in \mathrm{V}$$
4		difss	$$⊢A\setminus F\left[x\right]\subseteq A$$
5		elpw2g	$$⊢A\in \mathrm{V}\to \left(A\setminus F\left[x\right]\in 𝒫A\leftrightarrow A\setminus F\left[x\right]\subseteq A\right)$$
6	4 5	mpbiri	$$⊢A\in \mathrm{V}\to A\setminus F\left[x\right]\in 𝒫A$$
7		neeq1	$$⊢y=A\setminus F\left[x\right]\to \left(y\ne \varnothing \leftrightarrow A\setminus F\left[x\right]\ne \varnothing \right)$$
8		fveq2	$$⊢y=A\setminus F\left[x\right]\to g\left(y\right)=g\left(A\setminus F\left[x\right]\right)$$
9		id	$$⊢y=A\setminus F\left[x\right]\to y=A\setminus F\left[x\right]$$
10	8 9	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)$$
11	7 10	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)$$
12	11	rspcv	$$⊢A\setminus F\left[x\right]\in 𝒫A\to \left(\forall y\in 𝒫A\left(y\ne \varnothing \to g\left(y\right)\in y\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)\right)$$
13	6 12	syl	$$⊢A\in \mathrm{V}\to \left(\forall y\in 𝒫A\left(y\ne \varnothing \to g\left(y\right)\in y\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)\right)$$
14	13	3imp	$$⊢\left(A\in \mathrm{V}\wedge \forall y\in 𝒫A\left(y\ne \varnothing \to g\left(y\right)\in y\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)$$
15	1	tfr2	$$⊢x\in \mathrm{On}\to F\left(x\right)=G\left({F\upharpoonright }_x\right)$$
16	1	tfr1	$$⊢FFn\mathrm{On}$$
17		fnfun	$$⊢FFn\mathrm{On}\to \mathrm{Fun}F$$
18	16 17	ax-mp	$$⊢\mathrm{Fun}F$$
19		vex	$$⊢x\in \mathrm{V}$$
20		resfunexg	$$⊢\left(\mathrm{Fun}F\wedge x\in \mathrm{V}\right)\to {F\upharpoonright }_x\in \mathrm{V}$$
21	18 19 20	mp2an	$$⊢{F\upharpoonright }_x\in \mathrm{V}$$
22		rneq	$$⊢f={F\upharpoonright }_x\to \mathrm{ran}f=\mathrm{ran}\left({F\upharpoonright }_x\right)$$
23		df-ima	$$⊢F\left[x\right]=\mathrm{ran}\left({F\upharpoonright }_x\right)$$
24	22 23	eqtr4di	$$⊢f={F\upharpoonright }_x\to \mathrm{ran}f=F\left[x\right]$$
25	24	difeq2d	$$⊢f={F\upharpoonright }_x\to A\setminus \mathrm{ran}f=A\setminus F\left[x\right]$$
26	25	fveq2d	$$⊢f={F\upharpoonright }_x\to g\left(A\setminus \mathrm{ran}f\right)=g\left(A\setminus F\left[x\right]\right)$$
27		fvex	$$⊢g\left(A\setminus F\left[x\right]\right)\in \mathrm{V}$$
28	26 2 27	fvmpt	$$⊢{F\upharpoonright }_x\in \mathrm{V}\to G\left({F\upharpoonright }_x\right)=g\left(A\setminus F\left[x\right]\right)$$
29	21 28	ax-mp	$$⊢G\left({F\upharpoonright }_x\right)=g\left(A\setminus F\left[x\right]\right)$$
30	15 29	eqtrdi	$$⊢x\in \mathrm{On}\to F\left(x\right)=g\left(A\setminus F\left[x\right]\right)$$
31	30	eleq1d	$$⊢x\in \mathrm{On}\to \left(F\left(x\right)\in \left(A\setminus F\left[x\right]\right)\leftrightarrow g\left(A\setminus F\left[x\right]\right)\in \left(A\setminus F\left[x\right]\right)\right)$$
32	14 31	syl5ibrcom	$$⊢\left(A\in \mathrm{V}\wedge \forall y\in 𝒫A\left(y\ne \varnothing \to g\left(y\right)\in y\right)\wedge A\setminus F\left[x\right]\ne \varnothing \right)\to \left(x\in \mathrm{On}\to F\left(x\right)\in \left(A\setminus F\left[x\right]\right)\right)$$
33	32	3expia	$$⊢\left(A\in \mathrm{V}\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 \left(x\in \mathrm{On}\to F\left(x\right)\in \left(A\setminus F\left[x\right]\right)\right)\right)$$
34	33	com23	$$⊢\left(A\in \mathrm{V}\wedge \forall y\in 𝒫A\left(y\ne \varnothing \to g\left(y\right)\in y\right)\right)\to \left(x\in \mathrm{On}\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)\right)$$
35	34	ralrimiv	$$⊢\left(A\in \mathrm{V}\wedge \forall y\in 𝒫A\left(y\ne \varnothing \to g\left(y\right)\in y\right)\right)\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)$$
36	35	ex	$$⊢A\in \mathrm{V}\to \left(\forall y\in 𝒫A\left(y\ne \varnothing \to g\left(y\right)\in y\right)\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)\right)$$
37	16	tz7.49c	$$⊢\left(A\in \mathrm{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$$
38	37	ex	$$⊢A\in \mathrm{V}\to \left(\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)\to \exists x\in \mathrm{On}\left({F\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}A\right)$$
39	19	f1oen	$$⊢\left({F\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}A\to x\approx A$$
40		isnumi	$$⊢\left(x\in \mathrm{On}\wedge x\approx A\right)\to A\in \mathrm{dom}\mathrm{card}$$
41	39 40	sylan2	$$⊢\left(x\in \mathrm{On}\wedge \left({F\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}A\right)\to A\in \mathrm{dom}\mathrm{card}$$
42	41	rexlimiva	$$⊢\exists x\in \mathrm{On}\left({F\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}A\to A\in \mathrm{dom}\mathrm{card}$$
43	38 42	syl6	$$⊢A\in \mathrm{V}\to \left(\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)\to A\in \mathrm{dom}\mathrm{card}\right)$$
44	36 43	syld	$$⊢A\in \mathrm{V}\to \left(\forall y\in 𝒫A\left(y\ne \varnothing \to g\left(y\right)\in y\right)\to A\in \mathrm{dom}\mathrm{card}\right)$$
45	3 44	syl	$$⊢A\in C\to \left(\forall y\in 𝒫A\left(y\ne \varnothing \to g\left(y\right)\in y\right)\to A\in \mathrm{dom}\mathrm{card}\right)$$
46	45	exlimdv	$$⊢A\in C\to \left(\exists g\forall y\in 𝒫A\left(y\ne \varnothing \to g\left(y\right)\in y\right)\to A\in \mathrm{dom}\mathrm{card}\right)$$