ackbijnn

Description: Translate the Ackermann bijection ackbij1 onto the positive integers. (Contributed by Mario Carneiro, 16-Jan-2015)

		Ref	Expression
	Hypothesis	ackbijnn.1	$⊢ F = (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ \sum_{y \in x} 2^{y})$
	Assertion	ackbijnn	$⊢ F : 𝒫 ℕ_{0} \cap Fin \underset{1-1 onto}{⟶} ℕ_{0}$

Proof

Step	Hyp	Ref	Expression
1		ackbijnn.1	$⊢ F = (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ \sum_{y \in x} 2^{y})$
2		hashgval2	$⊢ {\|.\| ↾}_{ω} = {rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}$
3	2	hashgf1o	$⊢ ({\|.\| ↾}_{ω}) : ω \underset{1-1 onto}{⟶} ℕ_{0}$
4		sneq	$⊢ w = y \to \{w\} = \{y\}$
5		pweq	$⊢ w = y \to 𝒫 w = 𝒫 y$
6	4 5	xpeq12d	$⊢ w = y \to \{w\} \times 𝒫 w = \{y\} \times 𝒫 y$
7	6	cbviunv	$⊢ ⋃_{w \in z} (\{w\} \times 𝒫 w) = ⋃_{y \in z} (\{y\} \times 𝒫 y)$
8		iuneq1	$⊢ z = x \to ⋃_{y \in z} (\{y\} \times 𝒫 y) = ⋃_{y \in x} (\{y\} \times 𝒫 y)$
9	7 8	eqtrid	$⊢ z = x \to ⋃_{w \in z} (\{w\} \times 𝒫 w) = ⋃_{y \in x} (\{y\} \times 𝒫 y)$
10	9	fveq2d	$⊢ z = x \to card (⋃_{w \in z} (\{w\} \times 𝒫 w)) = card (⋃_{y \in x} (\{y\} \times 𝒫 y))$
11	10	cbvmptv	$⊢ (z \in (𝒫 ω \cap Fin) ⟼ card (⋃_{w \in z} (\{w\} \times 𝒫 w))) = (x \in (𝒫 ω \cap Fin) ⟼ card (⋃_{y \in x} (\{y\} \times 𝒫 y)))$
12	11	ackbij1	$⊢ (z \in (𝒫 ω \cap Fin) ⟼ card (⋃_{w \in z} (\{w\} \times 𝒫 w))) : 𝒫 ω \cap Fin \underset{1-1 onto}{⟶} ω$
13		f1ocnv	$⊢ ({\|.\| ↾}_{ω}) : ω \underset{1-1 onto}{⟶} ℕ_{0} \to {({\|.\| ↾}_{ω})}^{-1} : ℕ_{0} \underset{1-1 onto}{⟶} ω$
14	3 13	ax-mp	$⊢ {({\|.\| ↾}_{ω})}^{-1} : ℕ_{0} \underset{1-1 onto}{⟶} ω$
15		f1opwfi	$⊢ {({\|.\| ↾}_{ω})}^{-1} : ℕ_{0} \underset{1-1 onto}{⟶} ω \to (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ {({\|.\| ↾}_{ω})}^{-1} [x]) : 𝒫 ℕ_{0} \cap Fin \underset{1-1 onto}{⟶} 𝒫 ω \cap Fin$
16	14 15	ax-mp	$⊢ (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ {({\|.\| ↾}_{ω})}^{-1} [x]) : 𝒫 ℕ_{0} \cap Fin \underset{1-1 onto}{⟶} 𝒫 ω \cap Fin$
17		f1oco	$⊢ ((z \in (𝒫 ω \cap Fin) ⟼ card (⋃_{w \in z} (\{w\} \times 𝒫 w))) : 𝒫 ω \cap Fin \underset{1-1 onto}{⟶} ω \land (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ {({\|.\| ↾}_{ω})}^{-1} [x]) : 𝒫 ℕ_{0} \cap Fin \underset{1-1 onto}{⟶} 𝒫 ω \cap Fin) \to ((z \in (𝒫 ω \cap Fin) ⟼ card (⋃_{w \in z} (\{w\} \times 𝒫 w))) \circ (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ {({\|.\| ↾}_{ω})}^{-1} [x])) : 𝒫 ℕ_{0} \cap Fin \underset{1-1 onto}{⟶} ω$
18	12 16 17	mp2an	$⊢ ((z \in (𝒫 ω \cap Fin) ⟼ card (⋃_{w \in z} (\{w\} \times 𝒫 w))) \circ (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ {({\|.\| ↾}_{ω})}^{-1} [x])) : 𝒫 ℕ_{0} \cap Fin \underset{1-1 onto}{⟶} ω$
19		f1oco	$⊢ (({\|.\| ↾}_{ω}) : ω \underset{1-1 onto}{⟶} ℕ_{0} \land ((z \in (𝒫 ω \cap Fin) ⟼ card (⋃_{w \in z} (\{w\} \times 𝒫 w))) \circ (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ {({\|.\| ↾}_{ω})}^{-1} [x])) : 𝒫 ℕ_{0} \cap Fin \underset{1-1 onto}{⟶} ω) \to (({\|.\| ↾}_{ω}) \circ ((z \in (𝒫 ω \cap Fin) ⟼ card (⋃_{w \in z} (\{w\} \times 𝒫 w))) \circ (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ {({\|.\| ↾}_{ω})}^{-1} [x]))) : 𝒫 ℕ_{0} \cap Fin \underset{1-1 onto}{⟶} ℕ_{0}$
20	3 18 19	mp2an	$⊢ (({\|.\| ↾}_{ω}) \circ ((z \in (𝒫 ω \cap Fin) ⟼ card (⋃_{w \in z} (\{w\} \times 𝒫 w))) \circ (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ {({\|.\| ↾}_{ω})}^{-1} [x]))) : 𝒫 ℕ_{0} \cap Fin \underset{1-1 onto}{⟶} ℕ_{0}$
21		inss2	$⊢ 𝒫 ω \cap Fin \subseteq Fin$
22		f1of	$⊢ (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ {({\|.\| ↾}_{ω})}^{-1} [x]) : 𝒫 ℕ_{0} \cap Fin \underset{1-1 onto}{⟶} 𝒫 ω \cap Fin \to (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ {({\|.\| ↾}_{ω})}^{-1} [x]) : 𝒫 ℕ_{0} \cap Fin ⟶ 𝒫 ω \cap Fin$
23	16 22	ax-mp	$⊢ (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ {({\|.\| ↾}_{ω})}^{-1} [x]) : 𝒫 ℕ_{0} \cap Fin ⟶ 𝒫 ω \cap Fin$
24		eqid	$⊢ (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ {({\|.\| ↾}_{ω})}^{-1} [x]) = (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ {({\|.\| ↾}_{ω})}^{-1} [x])$
25	24	fmpt	$⊢ \forall x \in (𝒫 ℕ_{0} \cap Fin) {({\|.\| ↾}_{ω})}^{-1} [x] \in (𝒫 ω \cap Fin) \leftrightarrow (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ {({\|.\| ↾}_{ω})}^{-1} [x]) : 𝒫 ℕ_{0} \cap Fin ⟶ 𝒫 ω \cap Fin$
26	23 25	mpbir	$⊢ \forall x \in (𝒫 ℕ_{0} \cap Fin) {({\|.\| ↾}_{ω})}^{-1} [x] \in (𝒫 ω \cap Fin)$
27	26	rspec	$⊢ x \in (𝒫 ℕ_{0} \cap Fin) \to {({\|.\| ↾}_{ω})}^{-1} [x] \in (𝒫 ω \cap Fin)$
28	21 27	sselid	$⊢ x \in (𝒫 ℕ_{0} \cap Fin) \to {({\|.\| ↾}_{ω})}^{-1} [x] \in Fin$
29		snfi	$⊢ \{w\} \in Fin$
30		cnvimass	$⊢ {({\|.\| ↾}_{ω})}^{-1} [x] \subseteq dom ({\|.\| ↾}_{ω})$
31		dmhashres	$⊢ dom ({\|.\| ↾}_{ω}) = ω$
32	30 31	sseqtri	$⊢ {({\|.\| ↾}_{ω})}^{-1} [x] \subseteq ω$
33		onfin2	$⊢ ω = On \cap Fin$
34		inss2	$⊢ On \cap Fin \subseteq Fin$
35	33 34	eqsstri	$⊢ ω \subseteq Fin$
36	32 35	sstri	$⊢ {({\|.\| ↾}_{ω})}^{-1} [x] \subseteq Fin$
37		simpr	$⊢ (x \in (𝒫 ℕ_{0} \cap Fin) \land w \in {({\|.\| ↾}_{ω})}^{-1} [x]) \to w \in {({\|.\| ↾}_{ω})}^{-1} [x]$
38	36 37	sselid	$⊢ (x \in (𝒫 ℕ_{0} \cap Fin) \land w \in {({\|.\| ↾}_{ω})}^{-1} [x]) \to w \in Fin$
39		pwfi	$⊢ w \in Fin \leftrightarrow 𝒫 w \in Fin$
40	38 39	sylib	$⊢ (x \in (𝒫 ℕ_{0} \cap Fin) \land w \in {({\|.\| ↾}_{ω})}^{-1} [x]) \to 𝒫 w \in Fin$
41		xpfi	$⊢ (\{w\} \in Fin \land 𝒫 w \in Fin) \to \{w\} \times 𝒫 w \in Fin$
42	29 40 41	sylancr	$⊢ (x \in (𝒫 ℕ_{0} \cap Fin) \land w \in {({\|.\| ↾}_{ω})}^{-1} [x]) \to \{w\} \times 𝒫 w \in Fin$
43	42	ralrimiva	$⊢ x \in (𝒫 ℕ_{0} \cap Fin) \to \forall w \in {({\|.\| ↾}_{ω})}^{-1} [x] \{w\} \times 𝒫 w \in Fin$
44		iunfi	$⊢ ({({\|.\| ↾}_{ω})}^{-1} [x] \in Fin \land \forall w \in {({\|.\| ↾}_{ω})}^{-1} [x] \{w\} \times 𝒫 w \in Fin) \to ⋃_{w \in {({\|.\| ↾}_{ω})}^{-1} [x]} (\{w\} \times 𝒫 w) \in Fin$
45	28 43 44	syl2anc	$⊢ x \in (𝒫 ℕ_{0} \cap Fin) \to ⋃_{w \in {({\|.\| ↾}_{ω})}^{-1} [x]} (\{w\} \times 𝒫 w) \in Fin$
46		ficardom	$⊢ ⋃_{w \in {({\|.\| ↾}_{ω})}^{-1} [x]} (\{w\} \times 𝒫 w) \in Fin \to card (⋃_{w \in {({\|.\| ↾}_{ω})}^{-1} [x]} (\{w\} \times 𝒫 w)) \in ω$
47	45 46	syl	$⊢ x \in (𝒫 ℕ_{0} \cap Fin) \to card (⋃_{w \in {({\|.\| ↾}_{ω})}^{-1} [x]} (\{w\} \times 𝒫 w)) \in ω$
48	47	fvresd	$⊢ x \in (𝒫 ℕ_{0} \cap Fin) \to ({\|.\| ↾}_{ω}) (card (⋃_{w \in {({\|.\| ↾}_{ω})}^{-1} [x]} (\{w\} \times 𝒫 w))) = \|card (⋃_{w \in {({\|.\| ↾}_{ω})}^{-1} [x]} (\{w\} \times 𝒫 w))\|$
49		hashcard	$⊢ ⋃_{w \in {({\|.\| ↾}_{ω})}^{-1} [x]} (\{w\} \times 𝒫 w) \in Fin \to \|card (⋃_{w \in {({\|.\| ↾}_{ω})}^{-1} [x]} (\{w\} \times 𝒫 w))\| = \|⋃_{w \in {({\|.\| ↾}_{ω})}^{-1} [x]} (\{w\} \times 𝒫 w)\|$
50	45 49	syl	$⊢ x \in (𝒫 ℕ_{0} \cap Fin) \to \|card (⋃_{w \in {({\|.\| ↾}_{ω})}^{-1} [x]} (\{w\} \times 𝒫 w))\| = \|⋃_{w \in {({\|.\| ↾}_{ω})}^{-1} [x]} (\{w\} \times 𝒫 w)\|$
51		xp1st	$⊢ z \in (\{w\} \times 𝒫 w) \to 1^{st} (z) \in \{w\}$
52		elsni	$⊢ 1^{st} (z) \in \{w\} \to 1^{st} (z) = w$
53	51 52	syl	$⊢ z \in (\{w\} \times 𝒫 w) \to 1^{st} (z) = w$
54	53	rgen	$⊢ \forall z \in (\{w\} \times 𝒫 w) 1^{st} (z) = w$
55	54	rgenw	$⊢ \forall w \in {({\|.\| ↾}_{ω})}^{-1} [x] \forall z \in (\{w\} \times 𝒫 w) 1^{st} (z) = w$
56		invdisj	$⊢ \forall w \in {({\|.\| ↾}_{ω})}^{-1} [x] \forall z \in (\{w\} \times 𝒫 w) 1^{st} (z) = w \to \underset{w \in {({\|.\| ↾}_{ω})}^{-1} [x]}{Disj} (\{w\} \times 𝒫 w)$
57	55 56	mp1i	$⊢ x \in (𝒫 ℕ_{0} \cap Fin) \to \underset{w \in {({\|.\| ↾}_{ω})}^{-1} [x]}{Disj} (\{w\} \times 𝒫 w)$
58	28 42 57	hashiun	$⊢ x \in (𝒫 ℕ_{0} \cap Fin) \to \|⋃_{w \in {({\|.\| ↾}_{ω})}^{-1} [x]} (\{w\} \times 𝒫 w)\| = \sum_{w \in {({\|.\| ↾}_{ω})}^{-1} [x]} \|\{w\} \times 𝒫 w\|$
59		sneq	$⊢ w = {({\|.\| ↾}_{ω})}^{-1} (y) \to \{w\} = \{{({\|.\| ↾}_{ω})}^{-1} (y)\}$
60		pweq	$⊢ w = {({\|.\| ↾}_{ω})}^{-1} (y) \to 𝒫 w = 𝒫 {({\|.\| ↾}_{ω})}^{-1} (y)$
61	59 60	xpeq12d	$⊢ w = {({\|.\| ↾}_{ω})}^{-1} (y) \to \{w\} \times 𝒫 w = \{{({\|.\| ↾}_{ω})}^{-1} (y)\} \times 𝒫 {({\|.\| ↾}_{ω})}^{-1} (y)$
62	61	fveq2d	$⊢ w = {({\|.\| ↾}_{ω})}^{-1} (y) \to \|\{w\} \times 𝒫 w\| = \|\{{({\|.\| ↾}_{ω})}^{-1} (y)\} \times 𝒫 {({\|.\| ↾}_{ω})}^{-1} (y)\|$
63		elinel2	$⊢ x \in (𝒫 ℕ_{0} \cap Fin) \to x \in Fin$
64		f1of1	$⊢ {({\|.\| ↾}_{ω})}^{-1} : ℕ_{0} \underset{1-1 onto}{⟶} ω \to {({\|.\| ↾}_{ω})}^{-1} : ℕ_{0} \underset{1-1}{⟶} ω$
65	14 64	ax-mp	$⊢ {({\|.\| ↾}_{ω})}^{-1} : ℕ_{0} \underset{1-1}{⟶} ω$
66		elinel1	$⊢ x \in (𝒫 ℕ_{0} \cap Fin) \to x \in 𝒫 ℕ_{0}$
67	66	elpwid	$⊢ x \in (𝒫 ℕ_{0} \cap Fin) \to x \subseteq ℕ_{0}$
68		f1ores	$⊢ ({({\|.\| ↾}_{ω})}^{-1} : ℕ_{0} \underset{1-1}{⟶} ω \land x \subseteq ℕ_{0}) \to ({{({\|.\| ↾}_{ω})}^{-1} ↾}_{x}) : x \underset{1-1 onto}{⟶} {({\|.\| ↾}_{ω})}^{-1} [x]$
69	65 67 68	sylancr	$⊢ x \in (𝒫 ℕ_{0} \cap Fin) \to ({{({\|.\| ↾}_{ω})}^{-1} ↾}_{x}) : x \underset{1-1 onto}{⟶} {({\|.\| ↾}_{ω})}^{-1} [x]$
70		fvres	$⊢ y \in x \to ({{({\|.\| ↾}_{ω})}^{-1} ↾}_{x}) (y) = {({\|.\| ↾}_{ω})}^{-1} (y)$
71	70	adantl	$⊢ (x \in (𝒫 ℕ_{0} \cap Fin) \land y \in x) \to ({{({\|.\| ↾}_{ω})}^{-1} ↾}_{x}) (y) = {({\|.\| ↾}_{ω})}^{-1} (y)$
72		hashcl	$⊢ \{w\} \times 𝒫 w \in Fin \to \|\{w\} \times 𝒫 w\| \in ℕ_{0}$
73		nn0cn	$⊢ \|\{w\} \times 𝒫 w\| \in ℕ_{0} \to \|\{w\} \times 𝒫 w\| \in ℂ$
74	42 72 73	3syl	$⊢ (x \in (𝒫 ℕ_{0} \cap Fin) \land w \in {({\|.\| ↾}_{ω})}^{-1} [x]) \to \|\{w\} \times 𝒫 w\| \in ℂ$
75	62 63 69 71 74	fsumf1o	$⊢ x \in (𝒫 ℕ_{0} \cap Fin) \to \sum_{w \in {({\|.\| ↾}_{ω})}^{-1} [x]} \|\{w\} \times 𝒫 w\| = \sum_{y \in x} \|\{{({\|.\| ↾}_{ω})}^{-1} (y)\} \times 𝒫 {({\|.\| ↾}_{ω})}^{-1} (y)\|$
76		snfi	$⊢ \{{({\|.\| ↾}_{ω})}^{-1} (y)\} \in Fin$
77	67	sselda	$⊢ (x \in (𝒫 ℕ_{0} \cap Fin) \land y \in x) \to y \in ℕ_{0}$
78		f1of	$⊢ {({\|.\| ↾}_{ω})}^{-1} : ℕ_{0} \underset{1-1 onto}{⟶} ω \to {({\|.\| ↾}_{ω})}^{-1} : ℕ_{0} ⟶ ω$
79	14 78	ax-mp	$⊢ {({\|.\| ↾}_{ω})}^{-1} : ℕ_{0} ⟶ ω$
80	79	ffvelrni	$⊢ y \in ℕ_{0} \to {({\|.\| ↾}_{ω})}^{-1} (y) \in ω$
81	77 80	syl	$⊢ (x \in (𝒫 ℕ_{0} \cap Fin) \land y \in x) \to {({\|.\| ↾}_{ω})}^{-1} (y) \in ω$
82	35 81	sselid	$⊢ (x \in (𝒫 ℕ_{0} \cap Fin) \land y \in x) \to {({\|.\| ↾}_{ω})}^{-1} (y) \in Fin$
83		pwfi	$⊢ {({\|.\| ↾}_{ω})}^{-1} (y) \in Fin \leftrightarrow 𝒫 {({\|.\| ↾}_{ω})}^{-1} (y) \in Fin$
84	82 83	sylib	$⊢ (x \in (𝒫 ℕ_{0} \cap Fin) \land y \in x) \to 𝒫 {({\|.\| ↾}_{ω})}^{-1} (y) \in Fin$
85		hashxp	$⊢ (\{{({\|.\| ↾}_{ω})}^{-1} (y)\} \in Fin \land 𝒫 {({\|.\| ↾}_{ω})}^{-1} (y) \in Fin) \to \|\{{({\|.\| ↾}_{ω})}^{-1} (y)\} \times 𝒫 {({\|.\| ↾}_{ω})}^{-1} (y)\| = \|\{{({\|.\| ↾}_{ω})}^{-1} (y)\}\| \|𝒫 {({\|.\| ↾}_{ω})}^{-1} (y)\|$
86	76 84 85	sylancr	$⊢ (x \in (𝒫 ℕ_{0} \cap Fin) \land y \in x) \to \|\{{({\|.\| ↾}_{ω})}^{-1} (y)\} \times 𝒫 {({\|.\| ↾}_{ω})}^{-1} (y)\| = \|\{{({\|.\| ↾}_{ω})}^{-1} (y)\}\| \|𝒫 {({\|.\| ↾}_{ω})}^{-1} (y)\|$
87		hashsng	$⊢ {({\|.\| ↾}_{ω})}^{-1} (y) \in ω \to \|\{{({\|.\| ↾}_{ω})}^{-1} (y)\}\| = 1$
88	81 87	syl	$⊢ (x \in (𝒫 ℕ_{0} \cap Fin) \land y \in x) \to \|\{{({\|.\| ↾}_{ω})}^{-1} (y)\}\| = 1$
89		hashpw	$⊢ {({\|.\| ↾}_{ω})}^{-1} (y) \in Fin \to \|𝒫 {({\|.\| ↾}_{ω})}^{-1} (y)\| = 2^{\|{({\|.\| ↾}_{ω})}^{-1} (y)\|}$
90	82 89	syl	$⊢ (x \in (𝒫 ℕ_{0} \cap Fin) \land y \in x) \to \|𝒫 {({\|.\| ↾}_{ω})}^{-1} (y)\| = 2^{\|{({\|.\| ↾}_{ω})}^{-1} (y)\|}$
91	81	fvresd	$⊢ (x \in (𝒫 ℕ_{0} \cap Fin) \land y \in x) \to ({\|.\| ↾}_{ω}) ({({\|.\| ↾}_{ω})}^{-1} (y)) = \|{({\|.\| ↾}_{ω})}^{-1} (y)\|$
92		f1ocnvfv2	$⊢ (({\|.\| ↾}_{ω}) : ω \underset{1-1 onto}{⟶} ℕ_{0} \land y \in ℕ_{0}) \to ({\|.\| ↾}_{ω}) ({({\|.\| ↾}_{ω})}^{-1} (y)) = y$
93	3 77 92	sylancr	$⊢ (x \in (𝒫 ℕ_{0} \cap Fin) \land y \in x) \to ({\|.\| ↾}_{ω}) ({({\|.\| ↾}_{ω})}^{-1} (y)) = y$
94	91 93	eqtr3d	$⊢ (x \in (𝒫 ℕ_{0} \cap Fin) \land y \in x) \to \|{({\|.\| ↾}_{ω})}^{-1} (y)\| = y$
95	94	oveq2d	$⊢ (x \in (𝒫 ℕ_{0} \cap Fin) \land y \in x) \to 2^{\|{({\|.\| ↾}_{ω})}^{-1} (y)\|} = 2^{y}$
96	90 95	eqtrd	$⊢ (x \in (𝒫 ℕ_{0} \cap Fin) \land y \in x) \to \|𝒫 {({\|.\| ↾}_{ω})}^{-1} (y)\| = 2^{y}$
97	88 96	oveq12d	$⊢ (x \in (𝒫 ℕ_{0} \cap Fin) \land y \in x) \to \|\{{({\|.\| ↾}_{ω})}^{-1} (y)\}\| \|𝒫 {({\|.\| ↾}_{ω})}^{-1} (y)\| = 1 2^{y}$
98		2cn	$⊢ 2 \in ℂ$
99		expcl	$⊢ (2 \in ℂ \land y \in ℕ_{0}) \to 2^{y} \in ℂ$
100	98 77 99	sylancr	$⊢ (x \in (𝒫 ℕ_{0} \cap Fin) \land y \in x) \to 2^{y} \in ℂ$
101	100	mulid2d	$⊢ (x \in (𝒫 ℕ_{0} \cap Fin) \land y \in x) \to 1 2^{y} = 2^{y}$
102	86 97 101	3eqtrd	$⊢ (x \in (𝒫 ℕ_{0} \cap Fin) \land y \in x) \to \|\{{({\|.\| ↾}_{ω})}^{-1} (y)\} \times 𝒫 {({\|.\| ↾}_{ω})}^{-1} (y)\| = 2^{y}$
103	102	sumeq2dv	$⊢ x \in (𝒫 ℕ_{0} \cap Fin) \to \sum_{y \in x} \|\{{({\|.\| ↾}_{ω})}^{-1} (y)\} \times 𝒫 {({\|.\| ↾}_{ω})}^{-1} (y)\| = \sum_{y \in x} 2^{y}$
104	58 75 103	3eqtrd	$⊢ x \in (𝒫 ℕ_{0} \cap Fin) \to \|⋃_{w \in {({\|.\| ↾}_{ω})}^{-1} [x]} (\{w\} \times 𝒫 w)\| = \sum_{y \in x} 2^{y}$
105	48 50 104	3eqtrd	$⊢ x \in (𝒫 ℕ_{0} \cap Fin) \to ({\|.\| ↾}_{ω}) (card (⋃_{w \in {({\|.\| ↾}_{ω})}^{-1} [x]} (\{w\} \times 𝒫 w))) = \sum_{y \in x} 2^{y}$
106	105	mpteq2ia	$⊢ (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ ({\|.\| ↾}_{ω}) (card (⋃_{w \in {({\|.\| ↾}_{ω})}^{-1} [x]} (\{w\} \times 𝒫 w)))) = (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ \sum_{y \in x} 2^{y})$
107	47	adantl	$⊢ (⊤ \land x \in (𝒫 ℕ_{0} \cap Fin)) \to card (⋃_{w \in {({\|.\| ↾}_{ω})}^{-1} [x]} (\{w\} \times 𝒫 w)) \in ω$
108	27	adantl	$⊢ (⊤ \land x \in (𝒫 ℕ_{0} \cap Fin)) \to {({\|.\| ↾}_{ω})}^{-1} [x] \in (𝒫 ω \cap Fin)$
109		eqidd	$⊢ ⊤ \to (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ {({\|.\| ↾}_{ω})}^{-1} [x]) = (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ {({\|.\| ↾}_{ω})}^{-1} [x])$
110		eqidd	$⊢ ⊤ \to (z \in (𝒫 ω \cap Fin) ⟼ card (⋃_{w \in z} (\{w\} \times 𝒫 w))) = (z \in (𝒫 ω \cap Fin) ⟼ card (⋃_{w \in z} (\{w\} \times 𝒫 w)))$
111		iuneq1	$⊢ z = {({\|.\| ↾}_{ω})}^{-1} [x] \to ⋃_{w \in z} (\{w\} \times 𝒫 w) = ⋃_{w \in {({\|.\| ↾}_{ω})}^{-1} [x]} (\{w\} \times 𝒫 w)$
112	111	fveq2d	$⊢ z = {({\|.\| ↾}_{ω})}^{-1} [x] \to card (⋃_{w \in z} (\{w\} \times 𝒫 w)) = card (⋃_{w \in {({\|.\| ↾}_{ω})}^{-1} [x]} (\{w\} \times 𝒫 w))$
113	108 109 110 112	fmptco	$⊢ ⊤ \to (z \in (𝒫 ω \cap Fin) ⟼ card (⋃_{w \in z} (\{w\} \times 𝒫 w))) \circ (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ {({\|.\| ↾}_{ω})}^{-1} [x]) = (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ card (⋃_{w \in {({\|.\| ↾}_{ω})}^{-1} [x]} (\{w\} \times 𝒫 w)))$
114		f1of	$⊢ ({\|.\| ↾}_{ω}) : ω \underset{1-1 onto}{⟶} ℕ_{0} \to ({\|.\| ↾}_{ω}) : ω ⟶ ℕ_{0}$
115	3 114	mp1i	$⊢ ⊤ \to ({\|.\| ↾}_{ω}) : ω ⟶ ℕ_{0}$
116	115	feqmptd	$⊢ ⊤ \to {\|.\| ↾}_{ω} = (y \in ω ⟼ ({\|.\| ↾}_{ω}) (y))$
117		fveq2	$⊢ y = card (⋃_{w \in {({\|.\| ↾}_{ω})}^{-1} [x]} (\{w\} \times 𝒫 w)) \to ({\|.\| ↾}_{ω}) (y) = ({\|.\| ↾}_{ω}) (card (⋃_{w \in {({\|.\| ↾}_{ω})}^{-1} [x]} (\{w\} \times 𝒫 w)))$
118	107 113 116 117	fmptco	$⊢ ⊤ \to ({\|.\| ↾}_{ω}) \circ ((z \in (𝒫 ω \cap Fin) ⟼ card (⋃_{w \in z} (\{w\} \times 𝒫 w))) \circ (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ {({\|.\| ↾}_{ω})}^{-1} [x])) = (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ ({\|.\| ↾}_{ω}) (card (⋃_{w \in {({\|.\| ↾}_{ω})}^{-1} [x]} (\{w\} \times 𝒫 w))))$
119	118	mptru	$⊢ ({\|.\| ↾}_{ω}) \circ ((z \in (𝒫 ω \cap Fin) ⟼ card (⋃_{w \in z} (\{w\} \times 𝒫 w))) \circ (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ {({\|.\| ↾}_{ω})}^{-1} [x])) = (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ ({\|.\| ↾}_{ω}) (card (⋃_{w \in {({\|.\| ↾}_{ω})}^{-1} [x]} (\{w\} \times 𝒫 w))))$
120	106 119 1	3eqtr4i	$⊢ ({\|.\| ↾}_{ω}) \circ ((z \in (𝒫 ω \cap Fin) ⟼ card (⋃_{w \in z} (\{w\} \times 𝒫 w))) \circ (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ {({\|.\| ↾}_{ω})}^{-1} [x])) = F$
121		f1oeq1	$⊢ ({\|.\| ↾}_{ω}) \circ ((z \in (𝒫 ω \cap Fin) ⟼ card (⋃_{w \in z} (\{w\} \times 𝒫 w))) \circ (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ {({\|.\| ↾}_{ω})}^{-1} [x])) = F \to ((({\|.\| ↾}_{ω}) \circ ((z \in (𝒫 ω \cap Fin) ⟼ card (⋃_{w \in z} (\{w\} \times 𝒫 w))) \circ (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ {({\|.\| ↾}_{ω})}^{-1} [x]))) : 𝒫 ℕ_{0} \cap Fin \underset{1-1 onto}{⟶} ℕ_{0} \leftrightarrow F : 𝒫 ℕ_{0} \cap Fin \underset{1-1 onto}{⟶} ℕ_{0})$
122	120 121	ax-mp	$⊢ (({\|.\| ↾}_{ω}) \circ ((z \in (𝒫 ω \cap Fin) ⟼ card (⋃_{w \in z} (\{w\} \times 𝒫 w))) \circ (x \in (𝒫 ℕ_{0} \cap Fin) ⟼ {({\|.\| ↾}_{ω})}^{-1} [x]))) : 𝒫 ℕ_{0} \cap Fin \underset{1-1 onto}{⟶} ℕ_{0} \leftrightarrow F : 𝒫 ℕ_{0} \cap Fin \underset{1-1 onto}{⟶} ℕ_{0}$
123	20 122	mpbi	$⊢ F : 𝒫 ℕ_{0} \cap Fin \underset{1-1 onto}{⟶} ℕ_{0}$

Metamath Proof Explorer

Theorem ackbijnn

Proof