Theorem ackbij1b

Description: The Ackermann bijection, part 1b: the bijection from ackbij1 restricts naturally to the powers of particular naturals. (Contributed by Stefan O'Rear, 18-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	ackbij1b	$$⊢A\in \mathrm{\omega }\to F\left[𝒫A\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	1	ackbij1lem17	$$⊢F:𝒫\mathrm{\omega }\cap \mathrm{Fin}\underset{1-1}{⟶}\mathrm{\omega }$$
3		ackbij2lem1	$$⊢A\in \mathrm{\omega }\to 𝒫A\subseteq 𝒫\mathrm{\omega }\cap \mathrm{Fin}$$
4		pwexg	$$⊢A\in \mathrm{\omega }\to 𝒫A\in \mathrm{V}$$
5		f1imaeng	$$⊢\left(F:𝒫\mathrm{\omega }\cap \mathrm{Fin}\underset{1-1}{⟶}\mathrm{\omega }\wedge 𝒫A\subseteq 𝒫\mathrm{\omega }\cap \mathrm{Fin}\wedge 𝒫A\in \mathrm{V}\right)\to F\left[𝒫A\right]\approx 𝒫A$$
6	2 3 4 5	mp3an2i	$$⊢A\in \mathrm{\omega }\to F\left[𝒫A\right]\approx 𝒫A$$
7		nnfi	$$⊢A\in \mathrm{\omega }\to A\in \mathrm{Fin}$$
8		pwfi	$$⊢A\in \mathrm{Fin}\leftrightarrow 𝒫A\in \mathrm{Fin}$$
9	7 8	sylib	$$⊢A\in \mathrm{\omega }\to 𝒫A\in \mathrm{Fin}$$
10		ficardid	$$⊢𝒫A\in \mathrm{Fin}\to \mathrm{card}\left(𝒫A\right)\approx 𝒫A$$
11		ensym	$$⊢\mathrm{card}\left(𝒫A\right)\approx 𝒫A\to 𝒫A\approx \mathrm{card}\left(𝒫A\right)$$
12	9 10 11	3syl	$$⊢A\in \mathrm{\omega }\to 𝒫A\approx \mathrm{card}\left(𝒫A\right)$$
13		entr	$$⊢\left(F\left[𝒫A\right]\approx 𝒫A\wedge 𝒫A\approx \mathrm{card}\left(𝒫A\right)\right)\to F\left[𝒫A\right]\approx \mathrm{card}\left(𝒫A\right)$$
14	6 12 13	syl2anc	$$⊢A\in \mathrm{\omega }\to F\left[𝒫A\right]\approx \mathrm{card}\left(𝒫A\right)$$
15		onfin2	$$⊢\mathrm{\omega }=\mathrm{On}\cap \mathrm{Fin}$$
16		inss2	$$⊢\mathrm{On}\cap \mathrm{Fin}\subseteq \mathrm{Fin}$$
17	15 16	eqsstri	$$⊢\mathrm{\omega }\subseteq \mathrm{Fin}$$
18		ficardom	$$⊢𝒫A\in \mathrm{Fin}\to \mathrm{card}\left(𝒫A\right)\in \mathrm{\omega }$$
19	9 18	syl	$$⊢A\in \mathrm{\omega }\to \mathrm{card}\left(𝒫A\right)\in \mathrm{\omega }$$
20	17 19	sselid	$$⊢A\in \mathrm{\omega }\to \mathrm{card}\left(𝒫A\right)\in \mathrm{Fin}$$
21		php3	$$⊢\left(\mathrm{card}\left(𝒫A\right)\in \mathrm{Fin}\wedge F\left[𝒫A\right]\subset \mathrm{card}\left(𝒫A\right)\right)\to F\left[𝒫A\right]\prec \mathrm{card}\left(𝒫A\right)$$
22	21	ex	$$⊢\mathrm{card}\left(𝒫A\right)\in \mathrm{Fin}\to \left(F\left[𝒫A\right]\subset \mathrm{card}\left(𝒫A\right)\to F\left[𝒫A\right]\prec \mathrm{card}\left(𝒫A\right)\right)$$
23	20 22	syl	$$⊢A\in \mathrm{\omega }\to \left(F\left[𝒫A\right]\subset \mathrm{card}\left(𝒫A\right)\to F\left[𝒫A\right]\prec \mathrm{card}\left(𝒫A\right)\right)$$
24		sdomnen	$$⊢F\left[𝒫A\right]\prec \mathrm{card}\left(𝒫A\right)\to \neg F\left[𝒫A\right]\approx \mathrm{card}\left(𝒫A\right)$$
25	23 24	syl6	$$⊢A\in \mathrm{\omega }\to \left(F\left[𝒫A\right]\subset \mathrm{card}\left(𝒫A\right)\to \neg F\left[𝒫A\right]\approx \mathrm{card}\left(𝒫A\right)\right)$$
26	14 25	mt2d	$$⊢A\in \mathrm{\omega }\to \neg F\left[𝒫A\right]\subset \mathrm{card}\left(𝒫A\right)$$
27		fvex	$$⊢F\left(a\right)\in \mathrm{V}$$
28		ackbij1lem3	$$⊢A\in \mathrm{\omega }\to A\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)$$
29		elpwi	$$⊢a\in 𝒫A\to a\subseteq A$$
30	1	ackbij1lem12	$$⊢\left(A\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge a\subseteq A\right)\to F\left(a\right)\subseteq F\left(A\right)$$
31	28 29 30	syl2an	$$⊢\left(A\in \mathrm{\omega }\wedge a\in 𝒫A\right)\to F\left(a\right)\subseteq F\left(A\right)$$
32	1	ackbij1lem10	$$⊢F:𝒫\mathrm{\omega }\cap \mathrm{Fin}⟶\mathrm{\omega }$$
33		peano1	$$⊢\varnothing \in \mathrm{\omega }$$
34	32 33	f0cli	$$⊢F\left(a\right)\in \mathrm{\omega }$$
35		nnord	$$⊢F\left(a\right)\in \mathrm{\omega }\to \mathrm{Ord}F\left(a\right)$$
36	34 35	ax-mp	$$⊢\mathrm{Ord}F\left(a\right)$$
37	32 33	f0cli	$$⊢F\left(A\right)\in \mathrm{\omega }$$
38		nnord	$$⊢F\left(A\right)\in \mathrm{\omega }\to \mathrm{Ord}F\left(A\right)$$
39	37 38	ax-mp	$$⊢\mathrm{Ord}F\left(A\right)$$
40		ordsucsssuc	$$⊢\left(\mathrm{Ord}F\left(a\right)\wedge \mathrm{Ord}F\left(A\right)\right)\to \left(F\left(a\right)\subseteq F\left(A\right)\leftrightarrow \mathrm{suc}F\left(a\right)\subseteq \mathrm{suc}F\left(A\right)\right)$$
41	36 39 40	mp2an	$$⊢F\left(a\right)\subseteq F\left(A\right)\leftrightarrow \mathrm{suc}F\left(a\right)\subseteq \mathrm{suc}F\left(A\right)$$
42	31 41	sylib	$$⊢\left(A\in \mathrm{\omega }\wedge a\in 𝒫A\right)\to \mathrm{suc}F\left(a\right)\subseteq \mathrm{suc}F\left(A\right)$$
43	1	ackbij1lem14	$$⊢A\in \mathrm{\omega }\to F\left(\left\{A\right\}\right)=\mathrm{suc}F\left(A\right)$$
44	1	ackbij1lem8	$$⊢A\in \mathrm{\omega }\to F\left(\left\{A\right\}\right)=\mathrm{card}\left(𝒫A\right)$$
45	43 44	eqtr3d	$$⊢A\in \mathrm{\omega }\to \mathrm{suc}F\left(A\right)=\mathrm{card}\left(𝒫A\right)$$
46	45	adantr	$$⊢\left(A\in \mathrm{\omega }\wedge a\in 𝒫A\right)\to \mathrm{suc}F\left(A\right)=\mathrm{card}\left(𝒫A\right)$$
47	42 46	sseqtrd	$$⊢\left(A\in \mathrm{\omega }\wedge a\in 𝒫A\right)\to \mathrm{suc}F\left(a\right)\subseteq \mathrm{card}\left(𝒫A\right)$$
48		sucssel	$$⊢F\left(a\right)\in \mathrm{V}\to \left(\mathrm{suc}F\left(a\right)\subseteq \mathrm{card}\left(𝒫A\right)\to F\left(a\right)\in \mathrm{card}\left(𝒫A\right)\right)$$
49	27 47 48	mpsyl	$$⊢\left(A\in \mathrm{\omega }\wedge a\in 𝒫A\right)\to F\left(a\right)\in \mathrm{card}\left(𝒫A\right)$$
50	49	ralrimiva	$$⊢A\in \mathrm{\omega }\to \forall a\in 𝒫AF\left(a\right)\in \mathrm{card}\left(𝒫A\right)$$
51		f1fun	$$⊢F:𝒫\mathrm{\omega }\cap \mathrm{Fin}\underset{1-1}{⟶}\mathrm{\omega }\to \mathrm{Fun}F$$
52	2 51	ax-mp	$$⊢\mathrm{Fun}F$$
53		f1dm	$$⊢F:𝒫\mathrm{\omega }\cap \mathrm{Fin}\underset{1-1}{⟶}\mathrm{\omega }\to \mathrm{dom}F=𝒫\mathrm{\omega }\cap \mathrm{Fin}$$
54	2 53	ax-mp	$$⊢\mathrm{dom}F=𝒫\mathrm{\omega }\cap \mathrm{Fin}$$
55	3 54	sseqtrrdi	$$⊢A\in \mathrm{\omega }\to 𝒫A\subseteq \mathrm{dom}F$$
56		funimass4	$$⊢\left(\mathrm{Fun}F\wedge 𝒫A\subseteq \mathrm{dom}F\right)\to \left(F\left[𝒫A\right]\subseteq \mathrm{card}\left(𝒫A\right)\leftrightarrow \forall a\in 𝒫AF\left(a\right)\in \mathrm{card}\left(𝒫A\right)\right)$$
57	52 55 56	sylancr	$$⊢A\in \mathrm{\omega }\to \left(F\left[𝒫A\right]\subseteq \mathrm{card}\left(𝒫A\right)\leftrightarrow \forall a\in 𝒫AF\left(a\right)\in \mathrm{card}\left(𝒫A\right)\right)$$
58	50 57	mpbird	$$⊢A\in \mathrm{\omega }\to F\left[𝒫A\right]\subseteq \mathrm{card}\left(𝒫A\right)$$
59		sspss	$$⊢F\left[𝒫A\right]\subseteq \mathrm{card}\left(𝒫A\right)\leftrightarrow \left(F\left[𝒫A\right]\subset \mathrm{card}\left(𝒫A\right)\vee F\left[𝒫A\right]=\mathrm{card}\left(𝒫A\right)\right)$$
60	58 59	sylib	$$⊢A\in \mathrm{\omega }\to \left(F\left[𝒫A\right]\subset \mathrm{card}\left(𝒫A\right)\vee F\left[𝒫A\right]=\mathrm{card}\left(𝒫A\right)\right)$$
61		orel1	$$⊢\neg F\left[𝒫A\right]\subset \mathrm{card}\left(𝒫A\right)\to \left(\left(F\left[𝒫A\right]\subset \mathrm{card}\left(𝒫A\right)\vee F\left[𝒫A\right]=\mathrm{card}\left(𝒫A\right)\right)\to F\left[𝒫A\right]=\mathrm{card}\left(𝒫A\right)\right)$$
62	26 60 61	sylc	$$⊢A\in \mathrm{\omega }\to F\left[𝒫A\right]=\mathrm{card}\left(𝒫A\right)$$