Theorem ackbij1lem8

Description: Lemma for ackbij1 . (Contributed by Stefan O'Rear, 19-Nov-2014)

	Ref	Expression
Hypothesis	ackbij.f	$$⊢F=\left(x\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{y\in x}\left(\left\{y\right\}\times 𝒫y\right)\right)\right)$$
Assertion	ackbij1lem8	$$⊢A\in \mathrm{\omega }\to F\left(\left\{A\right\}\right)=\mathrm{card}\left(𝒫A\right)$$

Proof

Step	Hyp	Ref	Expression
1		ackbij.f	$$⊢F=\left(x\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{y\in x}\left(\left\{y\right\}\times 𝒫y\right)\right)\right)$$
2		sneq	$$⊢a=A\to \left\{a\right\}=\left\{A\right\}$$
3	2	fveq2d	$$⊢a=A\to F\left(\left\{a\right\}\right)=F\left(\left\{A\right\}\right)$$
4		pweq	$$⊢a=A\to 𝒫a=𝒫A$$
5	4	fveq2d	$$⊢a=A\to \mathrm{card}\left(𝒫a\right)=\mathrm{card}\left(𝒫A\right)$$
6	3 5	eqeq12d	$$⊢a=A\to \left(F\left(\left\{a\right\}\right)=\mathrm{card}\left(𝒫a\right)\leftrightarrow F\left(\left\{A\right\}\right)=\mathrm{card}\left(𝒫A\right)\right)$$
7		ackbij1lem4	$$⊢a\in \mathrm{\omega }\to \left\{a\right\}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)$$
8	1	ackbij1lem7	$$⊢\left\{a\right\}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to F\left(\left\{a\right\}\right)=\mathrm{card}\left(\bigcup _{y\in \left\{a\right\}}\left(\left\{y\right\}\times 𝒫y\right)\right)$$
9	7 8	syl	$$⊢a\in \mathrm{\omega }\to F\left(\left\{a\right\}\right)=\mathrm{card}\left(\bigcup _{y\in \left\{a\right\}}\left(\left\{y\right\}\times 𝒫y\right)\right)$$
10		vex	$$⊢a\in \mathrm{V}$$
11		sneq	$$⊢y=a\to \left\{y\right\}=\left\{a\right\}$$
12		pweq	$$⊢y=a\to 𝒫y=𝒫a$$
13	11 12	xpeq12d	$$⊢y=a\to \left\{y\right\}\times 𝒫y=\left\{a\right\}\times 𝒫a$$
14	10 13	iunxsn	$$⊢\bigcup _{y\in \left\{a\right\}}\left(\left\{y\right\}\times 𝒫y\right)=\left\{a\right\}\times 𝒫a$$
15	14	fveq2i	$$⊢\mathrm{card}\left(\bigcup _{y\in \left\{a\right\}}\left(\left\{y\right\}\times 𝒫y\right)\right)=\mathrm{card}\left(\left\{a\right\}\times 𝒫a\right)$$
16		vpwex	$$⊢𝒫a\in \mathrm{V}$$
17		xpsnen2g	$$⊢\left(a\in \mathrm{V}\wedge 𝒫a\in \mathrm{V}\right)\to \left(\left\{a\right\}\times 𝒫a\right)\approx 𝒫a$$
18	10 16 17	mp2an	$$⊢\left(\left\{a\right\}\times 𝒫a\right)\approx 𝒫a$$
19		carden2b	$$⊢\left(\left\{a\right\}\times 𝒫a\right)\approx 𝒫a\to \mathrm{card}\left(\left\{a\right\}\times 𝒫a\right)=\mathrm{card}\left(𝒫a\right)$$
20	18 19	ax-mp	$$⊢\mathrm{card}\left(\left\{a\right\}\times 𝒫a\right)=\mathrm{card}\left(𝒫a\right)$$
21	15 20	eqtri	$$⊢\mathrm{card}\left(\bigcup _{y\in \left\{a\right\}}\left(\left\{y\right\}\times 𝒫y\right)\right)=\mathrm{card}\left(𝒫a\right)$$
22	9 21	eqtrdi	$$⊢a\in \mathrm{\omega }\to F\left(\left\{a\right\}\right)=\mathrm{card}\left(𝒫a\right)$$
23	6 22	vtoclga	$$⊢A\in \mathrm{\omega }\to F\left(\left\{A\right\}\right)=\mathrm{card}\left(𝒫A\right)$$