ackbij2lem2

	Ref	Expression
Hypotheses	ackbij.f	$⊢ F = (x \in (𝒫 ω \cap Fin) ⟼ card (⋃_{y \in x} (\{y\} \times 𝒫 y)))$
	ackbij.g	$⊢ G = (x \in V ⟼ (y \in 𝒫 dom x ⟼ F (x [y])))$
Assertion	ackbij2lem2	$⊢ A \in ω \to rec (G, \emptyset) (A) : R_{1} (A) \underset{1-1 onto}{⟶} card (R_{1} (A))$

Proof

Step	Hyp	Ref	Expression
1		ackbij.f	$⊢ F = (x \in (𝒫 ω \cap Fin) ⟼ card (⋃_{y \in x} (\{y\} \times 𝒫 y)))$
2		ackbij.g	$⊢ G = (x \in V ⟼ (y \in 𝒫 dom x ⟼ F (x [y])))$
3		fveq2	$⊢ a = \emptyset \to rec (G, \emptyset) (a) = rec (G, \emptyset) (\emptyset)$
4		fveq2	$⊢ a = \emptyset \to R_{1} (a) = R_{1} (\emptyset)$
5		2fveq3	$⊢ a = \emptyset \to card (R_{1} (a)) = card (R_{1} (\emptyset))$
6	3 4 5	f1oeq123d	$⊢ a = \emptyset \to (rec (G, \emptyset) (a) : R_{1} (a) \underset{1-1 onto}{⟶} card (R_{1} (a)) \leftrightarrow rec (G, \emptyset) (\emptyset) : R_{1} (\emptyset) \underset{1-1 onto}{⟶} card (R_{1} (\emptyset)))$
7		fveq2	$⊢ a = b \to rec (G, \emptyset) (a) = rec (G, \emptyset) (b)$
8		fveq2	$⊢ a = b \to R_{1} (a) = R_{1} (b)$
9		2fveq3	$⊢ a = b \to card (R_{1} (a)) = card (R_{1} (b))$
10	7 8 9	f1oeq123d	$⊢ a = b \to (rec (G, \emptyset) (a) : R_{1} (a) \underset{1-1 onto}{⟶} card (R_{1} (a)) \leftrightarrow rec (G, \emptyset) (b) : R_{1} (b) \underset{1-1 onto}{⟶} card (R_{1} (b)))$
11		fveq2	$⊢ a = suc b \to rec (G, \emptyset) (a) = rec (G, \emptyset) (suc b)$
12		fveq2	$⊢ a = suc b \to R_{1} (a) = R_{1} (suc b)$
13		2fveq3	$⊢ a = suc b \to card (R_{1} (a)) = card (R_{1} (suc b))$
14	11 12 13	f1oeq123d	$⊢ a = suc b \to (rec (G, \emptyset) (a) : R_{1} (a) \underset{1-1 onto}{⟶} card (R_{1} (a)) \leftrightarrow rec (G, \emptyset) (suc b) : R_{1} (suc b) \underset{1-1 onto}{⟶} card (R_{1} (suc b)))$
15		fveq2	$⊢ a = A \to rec (G, \emptyset) (a) = rec (G, \emptyset) (A)$
16		fveq2	$⊢ a = A \to R_{1} (a) = R_{1} (A)$
17		2fveq3	$⊢ a = A \to card (R_{1} (a)) = card (R_{1} (A))$
18	15 16 17	f1oeq123d	$⊢ a = A \to (rec (G, \emptyset) (a) : R_{1} (a) \underset{1-1 onto}{⟶} card (R_{1} (a)) \leftrightarrow rec (G, \emptyset) (A) : R_{1} (A) \underset{1-1 onto}{⟶} card (R_{1} (A)))$
19		f1o0	$⊢ \emptyset : \emptyset \underset{1-1 onto}{⟶} \emptyset$
20		0ex	$⊢ \emptyset \in V$
21	20	rdg0	$⊢ rec (G, \emptyset) (\emptyset) = \emptyset$
22		f1oeq1	$⊢ rec (G, \emptyset) (\emptyset) = \emptyset \to (rec (G, \emptyset) (\emptyset) : R_{1} (\emptyset) \underset{1-1 onto}{⟶} card (R_{1} (\emptyset)) \leftrightarrow \emptyset : R_{1} (\emptyset) \underset{1-1 onto}{⟶} card (R_{1} (\emptyset)))$
23	21 22	ax-mp	$⊢ rec (G, \emptyset) (\emptyset) : R_{1} (\emptyset) \underset{1-1 onto}{⟶} card (R_{1} (\emptyset)) \leftrightarrow \emptyset : R_{1} (\emptyset) \underset{1-1 onto}{⟶} card (R_{1} (\emptyset))$
24		r10	$⊢ R_{1} (\emptyset) = \emptyset$
25	24	fveq2i	$⊢ card (R_{1} (\emptyset)) = card (\emptyset)$
26		card0	$⊢ card (\emptyset) = \emptyset$
27	25 26	eqtri	$⊢ card (R_{1} (\emptyset)) = \emptyset$
28		f1oeq23	$⊢ (R_{1} (\emptyset) = \emptyset \land card (R_{1} (\emptyset)) = \emptyset) \to (\emptyset : R_{1} (\emptyset) \underset{1-1 onto}{⟶} card (R_{1} (\emptyset)) \leftrightarrow \emptyset : \emptyset \underset{1-1 onto}{⟶} \emptyset)$
29	24 27 28	mp2an	$⊢ \emptyset : R_{1} (\emptyset) \underset{1-1 onto}{⟶} card (R_{1} (\emptyset)) \leftrightarrow \emptyset : \emptyset \underset{1-1 onto}{⟶} \emptyset$
30	23 29	bitri	$⊢ rec (G, \emptyset) (\emptyset) : R_{1} (\emptyset) \underset{1-1 onto}{⟶} card (R_{1} (\emptyset)) \leftrightarrow \emptyset : \emptyset \underset{1-1 onto}{⟶} \emptyset$
31	19 30	mpbir	$⊢ rec (G, \emptyset) (\emptyset) : R_{1} (\emptyset) \underset{1-1 onto}{⟶} card (R_{1} (\emptyset))$
32	1	ackbij1lem17	$⊢ F : 𝒫 ω \cap Fin \underset{1-1}{⟶} ω$
33	32	a1i	$⊢ b \in ω \to F : 𝒫 ω \cap Fin \underset{1-1}{⟶} ω$
34		r1fin	$⊢ b \in ω \to R_{1} (b) \in Fin$
35		ficardom	$⊢ R_{1} (b) \in Fin \to card (R_{1} (b)) \in ω$
36	34 35	syl	$⊢ b \in ω \to card (R_{1} (b)) \in ω$
37		ackbij2lem1	$⊢ card (R_{1} (b)) \in ω \to 𝒫 card (R_{1} (b)) \subseteq 𝒫 ω \cap Fin$
38	36 37	syl	$⊢ b \in ω \to 𝒫 card (R_{1} (b)) \subseteq 𝒫 ω \cap Fin$
39		f1ores	$⊢ (F : 𝒫 ω \cap Fin \underset{1-1}{⟶} ω \land 𝒫 card (R_{1} (b)) \subseteq 𝒫 ω \cap Fin) \to ({F ↾}_{𝒫 card (R_{1} (b))}) : 𝒫 card (R_{1} (b)) \underset{1-1 onto}{⟶} F [𝒫 card (R_{1} (b))]$
40	33 38 39	syl2anc	$⊢ b \in ω \to ({F ↾}_{𝒫 card (R_{1} (b))}) : 𝒫 card (R_{1} (b)) \underset{1-1 onto}{⟶} F [𝒫 card (R_{1} (b))]$
41	1	ackbij1b	$⊢ card (R_{1} (b)) \in ω \to F [𝒫 card (R_{1} (b))] = card (𝒫 card (R_{1} (b)))$
42	36 41	syl	$⊢ b \in ω \to F [𝒫 card (R_{1} (b))] = card (𝒫 card (R_{1} (b)))$
43		ficardid	$⊢ R_{1} (b) \in Fin \to card (R_{1} (b)) \approx R_{1} (b)$
44		pwen	$⊢ card (R_{1} (b)) \approx R_{1} (b) \to 𝒫 card (R_{1} (b)) \approx 𝒫 R_{1} (b)$
45		carden2b	$⊢ 𝒫 card (R_{1} (b)) \approx 𝒫 R_{1} (b) \to card (𝒫 card (R_{1} (b))) = card (𝒫 R_{1} (b))$
46	34 43 44 45	4syl	$⊢ b \in ω \to card (𝒫 card (R_{1} (b))) = card (𝒫 R_{1} (b))$
47	42 46	eqtrd	$⊢ b \in ω \to F [𝒫 card (R_{1} (b))] = card (𝒫 R_{1} (b))$
48	47	f1oeq3d	$⊢ b \in ω \to (({F ↾}_{𝒫 card (R_{1} (b))}) : 𝒫 card (R_{1} (b)) \underset{1-1 onto}{⟶} F [𝒫 card (R_{1} (b))] \leftrightarrow ({F ↾}_{𝒫 card (R_{1} (b))}) : 𝒫 card (R_{1} (b)) \underset{1-1 onto}{⟶} card (𝒫 R_{1} (b)))$
49	40 48	mpbid	$⊢ b \in ω \to ({F ↾}_{𝒫 card (R_{1} (b))}) : 𝒫 card (R_{1} (b)) \underset{1-1 onto}{⟶} card (𝒫 R_{1} (b))$
50	49	adantr	$⊢ (b \in ω \land rec (G, \emptyset) (b) : R_{1} (b) \underset{1-1 onto}{⟶} card (R_{1} (b))) \to ({F ↾}_{𝒫 card (R_{1} (b))}) : 𝒫 card (R_{1} (b)) \underset{1-1 onto}{⟶} card (𝒫 R_{1} (b))$
51		f1opw	$⊢ rec (G, \emptyset) (b) : R_{1} (b) \underset{1-1 onto}{⟶} card (R_{1} (b)) \to (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a]) : 𝒫 R_{1} (b) \underset{1-1 onto}{⟶} 𝒫 card (R_{1} (b))$
52	51	adantl	$⊢ (b \in ω \land rec (G, \emptyset) (b) : R_{1} (b) \underset{1-1 onto}{⟶} card (R_{1} (b))) \to (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a]) : 𝒫 R_{1} (b) \underset{1-1 onto}{⟶} 𝒫 card (R_{1} (b))$
53		f1oco	$⊢ (({F ↾}_{𝒫 card (R_{1} (b))}) : 𝒫 card (R_{1} (b)) \underset{1-1 onto}{⟶} card (𝒫 R_{1} (b)) \land (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a]) : 𝒫 R_{1} (b) \underset{1-1 onto}{⟶} 𝒫 card (R_{1} (b))) \to (({F ↾}_{𝒫 card (R_{1} (b))}) \circ (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a])) : 𝒫 R_{1} (b) \underset{1-1 onto}{⟶} card (𝒫 R_{1} (b))$
54	50 52 53	syl2anc	$⊢ (b \in ω \land rec (G, \emptyset) (b) : R_{1} (b) \underset{1-1 onto}{⟶} card (R_{1} (b))) \to (({F ↾}_{𝒫 card (R_{1} (b))}) \circ (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a])) : 𝒫 R_{1} (b) \underset{1-1 onto}{⟶} card (𝒫 R_{1} (b))$
55		frsuc	$⊢ b \in ω \to ({rec (G, \emptyset) ↾}_{ω}) (suc b) = G (({rec (G, \emptyset) ↾}_{ω}) (b))$
56		peano2	$⊢ b \in ω \to suc b \in ω$
57	56	fvresd	$⊢ b \in ω \to ({rec (G, \emptyset) ↾}_{ω}) (suc b) = rec (G, \emptyset) (suc b)$
58		fvres	$⊢ b \in ω \to ({rec (G, \emptyset) ↾}_{ω}) (b) = rec (G, \emptyset) (b)$
59	58	fveq2d	$⊢ b \in ω \to G (({rec (G, \emptyset) ↾}_{ω}) (b)) = G (rec (G, \emptyset) (b))$
60		fvex	$⊢ rec (G, \emptyset) (b) \in V$
61		dmeq	$⊢ x = rec (G, \emptyset) (b) \to dom x = dom rec (G, \emptyset) (b)$
62	61	pweqd	$⊢ x = rec (G, \emptyset) (b) \to 𝒫 dom x = 𝒫 dom rec (G, \emptyset) (b)$
63		imaeq1	$⊢ x = rec (G, \emptyset) (b) \to x [y] = rec (G, \emptyset) (b) [y]$
64	63	fveq2d	$⊢ x = rec (G, \emptyset) (b) \to F (x [y]) = F (rec (G, \emptyset) (b) [y])$
65	62 64	mpteq12dv	$⊢ x = rec (G, \emptyset) (b) \to (y \in 𝒫 dom x ⟼ F (x [y])) = (y \in 𝒫 dom rec (G, \emptyset) (b) ⟼ F (rec (G, \emptyset) (b) [y]))$
66	60	dmex	$⊢ dom rec (G, \emptyset) (b) \in V$
67	66	pwex	$⊢ 𝒫 dom rec (G, \emptyset) (b) \in V$
68	67	mptex	$⊢ (y \in 𝒫 dom rec (G, \emptyset) (b) ⟼ F (rec (G, \emptyset) (b) [y])) \in V$
69	65 2 68	fvmpt	$⊢ rec (G, \emptyset) (b) \in V \to G (rec (G, \emptyset) (b)) = (y \in 𝒫 dom rec (G, \emptyset) (b) ⟼ F (rec (G, \emptyset) (b) [y]))$
70	60 69	ax-mp	$⊢ G (rec (G, \emptyset) (b)) = (y \in 𝒫 dom rec (G, \emptyset) (b) ⟼ F (rec (G, \emptyset) (b) [y]))$
71	59 70	eqtrdi	$⊢ b \in ω \to G (({rec (G, \emptyset) ↾}_{ω}) (b)) = (y \in 𝒫 dom rec (G, \emptyset) (b) ⟼ F (rec (G, \emptyset) (b) [y]))$
72	55 57 71	3eqtr3d	$⊢ b \in ω \to rec (G, \emptyset) (suc b) = (y \in 𝒫 dom rec (G, \emptyset) (b) ⟼ F (rec (G, \emptyset) (b) [y]))$
73	72	adantr	$⊢ (b \in ω \land rec (G, \emptyset) (b) : R_{1} (b) \underset{1-1 onto}{⟶} card (R_{1} (b))) \to rec (G, \emptyset) (suc b) = (y \in 𝒫 dom rec (G, \emptyset) (b) ⟼ F (rec (G, \emptyset) (b) [y]))$
74		f1odm	$⊢ rec (G, \emptyset) (b) : R_{1} (b) \underset{1-1 onto}{⟶} card (R_{1} (b)) \to dom rec (G, \emptyset) (b) = R_{1} (b)$
75	74	adantl	$⊢ (b \in ω \land rec (G, \emptyset) (b) : R_{1} (b) \underset{1-1 onto}{⟶} card (R_{1} (b))) \to dom rec (G, \emptyset) (b) = R_{1} (b)$
76	75	pweqd	$⊢ (b \in ω \land rec (G, \emptyset) (b) : R_{1} (b) \underset{1-1 onto}{⟶} card (R_{1} (b))) \to 𝒫 dom rec (G, \emptyset) (b) = 𝒫 R_{1} (b)$
77	76	mpteq1d	$⊢ (b \in ω \land rec (G, \emptyset) (b) : R_{1} (b) \underset{1-1 onto}{⟶} card (R_{1} (b))) \to (y \in 𝒫 dom rec (G, \emptyset) (b) ⟼ F (rec (G, \emptyset) (b) [y])) = (y \in 𝒫 R_{1} (b) ⟼ F (rec (G, \emptyset) (b) [y]))$
78		fvex	$⊢ F (rec (G, \emptyset) (b) [y]) \in V$
79		eqid	$⊢ (y \in 𝒫 R_{1} (b) ⟼ F (rec (G, \emptyset) (b) [y])) = (y \in 𝒫 R_{1} (b) ⟼ F (rec (G, \emptyset) (b) [y]))$
80	78 79	fnmpti	$⊢ (y \in 𝒫 R_{1} (b) ⟼ F (rec (G, \emptyset) (b) [y])) Fn 𝒫 R_{1} (b)$
81	80	a1i	$⊢ (b \in ω \land rec (G, \emptyset) (b) : R_{1} (b) \underset{1-1 onto}{⟶} card (R_{1} (b))) \to (y \in 𝒫 R_{1} (b) ⟼ F (rec (G, \emptyset) (b) [y])) Fn 𝒫 R_{1} (b)$
82		f1ofn	$⊢ (({F ↾}_{𝒫 card (R_{1} (b))}) \circ (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a])) : 𝒫 R_{1} (b) \underset{1-1 onto}{⟶} card (𝒫 R_{1} (b)) \to (({F ↾}_{𝒫 card (R_{1} (b))}) \circ (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a])) Fn 𝒫 R_{1} (b)$
83	54 82	syl	$⊢ (b \in ω \land rec (G, \emptyset) (b) : R_{1} (b) \underset{1-1 onto}{⟶} card (R_{1} (b))) \to (({F ↾}_{𝒫 card (R_{1} (b))}) \circ (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a])) Fn 𝒫 R_{1} (b)$
84		f1of	$⊢ (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a]) : 𝒫 R_{1} (b) \underset{1-1 onto}{⟶} 𝒫 card (R_{1} (b)) \to (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a]) : 𝒫 R_{1} (b) ⟶ 𝒫 card (R_{1} (b))$
85	52 84	syl	$⊢ (b \in ω \land rec (G, \emptyset) (b) : R_{1} (b) \underset{1-1 onto}{⟶} card (R_{1} (b))) \to (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a]) : 𝒫 R_{1} (b) ⟶ 𝒫 card (R_{1} (b))$
86	85	ffvelcdmda	$⊢ ((b \in ω \land rec (G, \emptyset) (b) : R_{1} (b) \underset{1-1 onto}{⟶} card (R_{1} (b))) \land c \in 𝒫 R_{1} (b)) \to (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a]) (c) \in 𝒫 card (R_{1} (b))$
87	86	fvresd	$⊢ ((b \in ω \land rec (G, \emptyset) (b) : R_{1} (b) \underset{1-1 onto}{⟶} card (R_{1} (b))) \land c \in 𝒫 R_{1} (b)) \to ({F ↾}_{𝒫 card (R_{1} (b))}) ((a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a]) (c)) = F ((a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a]) (c))$
88		imaeq2	$⊢ a = c \to rec (G, \emptyset) (b) [a] = rec (G, \emptyset) (b) [c]$
89		eqid	$⊢ (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a]) = (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a])$
90	60	imaex	$⊢ rec (G, \emptyset) (b) [c] \in V$
91	88 89 90	fvmpt	$⊢ c \in 𝒫 R_{1} (b) \to (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a]) (c) = rec (G, \emptyset) (b) [c]$
92	91	adantl	$⊢ ((b \in ω \land rec (G, \emptyset) (b) : R_{1} (b) \underset{1-1 onto}{⟶} card (R_{1} (b))) \land c \in 𝒫 R_{1} (b)) \to (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a]) (c) = rec (G, \emptyset) (b) [c]$
93	92	fveq2d	$⊢ ((b \in ω \land rec (G, \emptyset) (b) : R_{1} (b) \underset{1-1 onto}{⟶} card (R_{1} (b))) \land c \in 𝒫 R_{1} (b)) \to F ((a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a]) (c)) = F (rec (G, \emptyset) (b) [c])$
94	87 93	eqtrd	$⊢ ((b \in ω \land rec (G, \emptyset) (b) : R_{1} (b) \underset{1-1 onto}{⟶} card (R_{1} (b))) \land c \in 𝒫 R_{1} (b)) \to ({F ↾}_{𝒫 card (R_{1} (b))}) ((a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a]) (c)) = F (rec (G, \emptyset) (b) [c])$
95		fvco3	$⊢ ((a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a]) : 𝒫 R_{1} (b) ⟶ 𝒫 card (R_{1} (b)) \land c \in 𝒫 R_{1} (b)) \to (({F ↾}_{𝒫 card (R_{1} (b))}) \circ (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a])) (c) = ({F ↾}_{𝒫 card (R_{1} (b))}) ((a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a]) (c))$
96	85 95	sylan	$⊢ ((b \in ω \land rec (G, \emptyset) (b) : R_{1} (b) \underset{1-1 onto}{⟶} card (R_{1} (b))) \land c \in 𝒫 R_{1} (b)) \to (({F ↾}_{𝒫 card (R_{1} (b))}) \circ (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a])) (c) = ({F ↾}_{𝒫 card (R_{1} (b))}) ((a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a]) (c))$
97		imaeq2	$⊢ y = c \to rec (G, \emptyset) (b) [y] = rec (G, \emptyset) (b) [c]$
98	97	fveq2d	$⊢ y = c \to F (rec (G, \emptyset) (b) [y]) = F (rec (G, \emptyset) (b) [c])$
99		fvex	$⊢ F (rec (G, \emptyset) (b) [c]) \in V$
100	98 79 99	fvmpt	$⊢ c \in 𝒫 R_{1} (b) \to (y \in 𝒫 R_{1} (b) ⟼ F (rec (G, \emptyset) (b) [y])) (c) = F (rec (G, \emptyset) (b) [c])$
101	100	adantl	$⊢ ((b \in ω \land rec (G, \emptyset) (b) : R_{1} (b) \underset{1-1 onto}{⟶} card (R_{1} (b))) \land c \in 𝒫 R_{1} (b)) \to (y \in 𝒫 R_{1} (b) ⟼ F (rec (G, \emptyset) (b) [y])) (c) = F (rec (G, \emptyset) (b) [c])$
102	94 96 101	3eqtr4rd	$⊢ ((b \in ω \land rec (G, \emptyset) (b) : R_{1} (b) \underset{1-1 onto}{⟶} card (R_{1} (b))) \land c \in 𝒫 R_{1} (b)) \to (y \in 𝒫 R_{1} (b) ⟼ F (rec (G, \emptyset) (b) [y])) (c) = (({F ↾}_{𝒫 card (R_{1} (b))}) \circ (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a])) (c)$
103	81 83 102	eqfnfvd	$⊢ (b \in ω \land rec (G, \emptyset) (b) : R_{1} (b) \underset{1-1 onto}{⟶} card (R_{1} (b))) \to (y \in 𝒫 R_{1} (b) ⟼ F (rec (G, \emptyset) (b) [y])) = ({F ↾}_{𝒫 card (R_{1} (b))}) \circ (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a])$
104	77 103	eqtrd	$⊢ (b \in ω \land rec (G, \emptyset) (b) : R_{1} (b) \underset{1-1 onto}{⟶} card (R_{1} (b))) \to (y \in 𝒫 dom rec (G, \emptyset) (b) ⟼ F (rec (G, \emptyset) (b) [y])) = ({F ↾}_{𝒫 card (R_{1} (b))}) \circ (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a])$
105	73 104	eqtrd	$⊢ (b \in ω \land rec (G, \emptyset) (b) : R_{1} (b) \underset{1-1 onto}{⟶} card (R_{1} (b))) \to rec (G, \emptyset) (suc b) = ({F ↾}_{𝒫 card (R_{1} (b))}) \circ (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a])$
106		f1oeq1	$⊢ rec (G, \emptyset) (suc b) = ({F ↾}_{𝒫 card (R_{1} (b))}) \circ (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a]) \to (rec (G, \emptyset) (suc b) : R_{1} (suc b) \underset{1-1 onto}{⟶} card (R_{1} (suc b)) \leftrightarrow (({F ↾}_{𝒫 card (R_{1} (b))}) \circ (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a])) : R_{1} (suc b) \underset{1-1 onto}{⟶} card (R_{1} (suc b)))$
107	105 106	syl	$⊢ (b \in ω \land rec (G, \emptyset) (b) : R_{1} (b) \underset{1-1 onto}{⟶} card (R_{1} (b))) \to (rec (G, \emptyset) (suc b) : R_{1} (suc b) \underset{1-1 onto}{⟶} card (R_{1} (suc b)) \leftrightarrow (({F ↾}_{𝒫 card (R_{1} (b))}) \circ (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a])) : R_{1} (suc b) \underset{1-1 onto}{⟶} card (R_{1} (suc b)))$
108		nnon	$⊢ b \in ω \to b \in On$
109		r1suc	$⊢ b \in On \to R_{1} (suc b) = 𝒫 R_{1} (b)$
110	108 109	syl	$⊢ b \in ω \to R_{1} (suc b) = 𝒫 R_{1} (b)$
111	110	fveq2d	$⊢ b \in ω \to card (R_{1} (suc b)) = card (𝒫 R_{1} (b))$
112		f1oeq23	$⊢ (R_{1} (suc b) = 𝒫 R_{1} (b) \land card (R_{1} (suc b)) = card (𝒫 R_{1} (b))) \to ((({F ↾}_{𝒫 card (R_{1} (b))}) \circ (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a])) : R_{1} (suc b) \underset{1-1 onto}{⟶} card (R_{1} (suc b)) \leftrightarrow (({F ↾}_{𝒫 card (R_{1} (b))}) \circ (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a])) : 𝒫 R_{1} (b) \underset{1-1 onto}{⟶} card (𝒫 R_{1} (b)))$
113	110 111 112	syl2anc	$⊢ b \in ω \to ((({F ↾}_{𝒫 card (R_{1} (b))}) \circ (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a])) : R_{1} (suc b) \underset{1-1 onto}{⟶} card (R_{1} (suc b)) \leftrightarrow (({F ↾}_{𝒫 card (R_{1} (b))}) \circ (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a])) : 𝒫 R_{1} (b) \underset{1-1 onto}{⟶} card (𝒫 R_{1} (b)))$
114	113	adantr	$⊢ (b \in ω \land rec (G, \emptyset) (b) : R_{1} (b) \underset{1-1 onto}{⟶} card (R_{1} (b))) \to ((({F ↾}_{𝒫 card (R_{1} (b))}) \circ (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a])) : R_{1} (suc b) \underset{1-1 onto}{⟶} card (R_{1} (suc b)) \leftrightarrow (({F ↾}_{𝒫 card (R_{1} (b))}) \circ (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a])) : 𝒫 R_{1} (b) \underset{1-1 onto}{⟶} card (𝒫 R_{1} (b)))$
115	107 114	bitrd	$⊢ (b \in ω \land rec (G, \emptyset) (b) : R_{1} (b) \underset{1-1 onto}{⟶} card (R_{1} (b))) \to (rec (G, \emptyset) (suc b) : R_{1} (suc b) \underset{1-1 onto}{⟶} card (R_{1} (suc b)) \leftrightarrow (({F ↾}_{𝒫 card (R_{1} (b))}) \circ (a \in 𝒫 R_{1} (b) ⟼ rec (G, \emptyset) (b) [a])) : 𝒫 R_{1} (b) \underset{1-1 onto}{⟶} card (𝒫 R_{1} (b)))$
116	54 115	mpbird	$⊢ (b \in ω \land rec (G, \emptyset) (b) : R_{1} (b) \underset{1-1 onto}{⟶} card (R_{1} (b))) \to rec (G, \emptyset) (suc b) : R_{1} (suc b) \underset{1-1 onto}{⟶} card (R_{1} (suc b))$
117	116	ex	$⊢ b \in ω \to (rec (G, \emptyset) (b) : R_{1} (b) \underset{1-1 onto}{⟶} card (R_{1} (b)) \to rec (G, \emptyset) (suc b) : R_{1} (suc b) \underset{1-1 onto}{⟶} card (R_{1} (suc b)))$
118	6 10 14 18 31 117	finds	$⊢ A \in ω \to rec (G, \emptyset) (A) : R_{1} (A) \underset{1-1 onto}{⟶} card (R_{1} (A))$

Metamath Proof Explorer

Theorem ackbij2lem2

Proof