ackbij2lem3

	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	ackbij2lem3	$⊢ A \in ω \to rec (G, \emptyset) (A) \subseteq rec (G, \emptyset) (suc 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		suceq	$⊢ a = \emptyset \to suc a = suc \emptyset$
5	4	fveq2d	$⊢ a = \emptyset \to rec (G, \emptyset) (suc a) = rec (G, \emptyset) (suc \emptyset)$
6		fveq2	$⊢ a = \emptyset \to R_{1} (a) = R_{1} (\emptyset)$
7	5 6	reseq12d	$⊢ a = \emptyset \to {rec (G, \emptyset) (suc a) ↾}_{R_{1} (a)} = {rec (G, \emptyset) (suc \emptyset) ↾}_{R_{1} (\emptyset)}$
8	3 7	eqeq12d	$⊢ a = \emptyset \to (rec (G, \emptyset) (a) = {rec (G, \emptyset) (suc a) ↾}_{R_{1} (a)} \leftrightarrow rec (G, \emptyset) (\emptyset) = {rec (G, \emptyset) (suc \emptyset) ↾}_{R_{1} (\emptyset)})$
9		fveq2	$⊢ a = b \to rec (G, \emptyset) (a) = rec (G, \emptyset) (b)$
10		suceq	$⊢ a = b \to suc a = suc b$
11	10	fveq2d	$⊢ a = b \to rec (G, \emptyset) (suc a) = rec (G, \emptyset) (suc b)$
12		fveq2	$⊢ a = b \to R_{1} (a) = R_{1} (b)$
13	11 12	reseq12d	$⊢ a = b \to {rec (G, \emptyset) (suc a) ↾}_{R_{1} (a)} = {rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}$
14	9 13	eqeq12d	$⊢ a = b \to (rec (G, \emptyset) (a) = {rec (G, \emptyset) (suc a) ↾}_{R_{1} (a)} \leftrightarrow rec (G, \emptyset) (b) = {rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)})$
15		fveq2	$⊢ a = suc b \to rec (G, \emptyset) (a) = rec (G, \emptyset) (suc b)$
16		suceq	$⊢ a = suc b \to suc a = suc suc b$
17	16	fveq2d	$⊢ a = suc b \to rec (G, \emptyset) (suc a) = rec (G, \emptyset) (suc suc b)$
18		fveq2	$⊢ a = suc b \to R_{1} (a) = R_{1} (suc b)$
19	17 18	reseq12d	$⊢ a = suc b \to {rec (G, \emptyset) (suc a) ↾}_{R_{1} (a)} = {rec (G, \emptyset) (suc suc b) ↾}_{R_{1} (suc b)}$
20	15 19	eqeq12d	$⊢ a = suc b \to (rec (G, \emptyset) (a) = {rec (G, \emptyset) (suc a) ↾}_{R_{1} (a)} \leftrightarrow rec (G, \emptyset) (suc b) = {rec (G, \emptyset) (suc suc b) ↾}_{R_{1} (suc b)})$
21		fveq2	$⊢ a = A \to rec (G, \emptyset) (a) = rec (G, \emptyset) (A)$
22		suceq	$⊢ a = A \to suc a = suc A$
23	22	fveq2d	$⊢ a = A \to rec (G, \emptyset) (suc a) = rec (G, \emptyset) (suc A)$
24		fveq2	$⊢ a = A \to R_{1} (a) = R_{1} (A)$
25	23 24	reseq12d	$⊢ a = A \to {rec (G, \emptyset) (suc a) ↾}_{R_{1} (a)} = {rec (G, \emptyset) (suc A) ↾}_{R_{1} (A)}$
26	21 25	eqeq12d	$⊢ a = A \to (rec (G, \emptyset) (a) = {rec (G, \emptyset) (suc a) ↾}_{R_{1} (a)} \leftrightarrow rec (G, \emptyset) (A) = {rec (G, \emptyset) (suc A) ↾}_{R_{1} (A)})$
27		res0	$⊢ {rec (G, \emptyset) (suc \emptyset) ↾}_{\emptyset} = \emptyset$
28		r10	$⊢ R_{1} (\emptyset) = \emptyset$
29	28	reseq2i	$⊢ {rec (G, \emptyset) (suc \emptyset) ↾}_{R_{1} (\emptyset)} = {rec (G, \emptyset) (suc \emptyset) ↾}_{\emptyset}$
30		0ex	$⊢ \emptyset \in V$
31	30	rdg0	$⊢ rec (G, \emptyset) (\emptyset) = \emptyset$
32	27 29 31	3eqtr4ri	$⊢ rec (G, \emptyset) (\emptyset) = {rec (G, \emptyset) (suc \emptyset) ↾}_{R_{1} (\emptyset)}$
33		peano2	$⊢ b \in ω \to suc b \in ω$
34	1 2	ackbij2lem2	$⊢ suc b \in ω \to rec (G, \emptyset) (suc b) : R_{1} (suc b) \underset{1-1 onto}{⟶} card (R_{1} (suc b))$
35	33 34	syl	$⊢ b \in ω \to rec (G, \emptyset) (suc b) : R_{1} (suc b) \underset{1-1 onto}{⟶} card (R_{1} (suc b))$
36		f1ofn	$⊢ rec (G, \emptyset) (suc b) : R_{1} (suc b) \underset{1-1 onto}{⟶} card (R_{1} (suc b)) \to rec (G, \emptyset) (suc b) Fn R_{1} (suc b)$
37	35 36	syl	$⊢ b \in ω \to rec (G, \emptyset) (suc b) Fn R_{1} (suc b)$
38	37	adantr	$⊢ (b \in ω \land rec (G, \emptyset) (b) = {rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) \to rec (G, \emptyset) (suc b) Fn R_{1} (suc b)$
39		peano2	$⊢ suc b \in ω \to suc suc b \in ω$
40	1 2	ackbij2lem2	$⊢ suc suc b \in ω \to rec (G, \emptyset) (suc suc b) : R_{1} (suc suc b) \underset{1-1 onto}{⟶} card (R_{1} (suc suc b))$
41		f1ofn	$⊢ rec (G, \emptyset) (suc suc b) : R_{1} (suc suc b) \underset{1-1 onto}{⟶} card (R_{1} (suc suc b)) \to rec (G, \emptyset) (suc suc b) Fn R_{1} (suc suc b)$
42	33 39 40 41	4syl	$⊢ b \in ω \to rec (G, \emptyset) (suc suc b) Fn R_{1} (suc suc b)$
43		nnon	$⊢ suc b \in ω \to suc b \in On$
44	33 43	syl	$⊢ b \in ω \to suc b \in On$
45		r1sssuc	$⊢ suc b \in On \to R_{1} (suc b) \subseteq R_{1} (suc suc b)$
46	44 45	syl	$⊢ b \in ω \to R_{1} (suc b) \subseteq R_{1} (suc suc b)$
47		fnssres	$⊢ (rec (G, \emptyset) (suc suc b) Fn R_{1} (suc suc b) \land R_{1} (suc b) \subseteq R_{1} (suc suc b)) \to ({rec (G, \emptyset) (suc suc b) ↾}_{R_{1} (suc b)}) Fn R_{1} (suc b)$
48	42 46 47	syl2anc	$⊢ b \in ω \to ({rec (G, \emptyset) (suc suc b) ↾}_{R_{1} (suc b)}) Fn R_{1} (suc b)$
49	48	adantr	$⊢ (b \in ω \land rec (G, \emptyset) (b) = {rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) \to ({rec (G, \emptyset) (suc suc b) ↾}_{R_{1} (suc b)}) Fn R_{1} (suc b)$
50		nnon	$⊢ b \in ω \to b \in On$
51		r1suc	$⊢ b \in On \to R_{1} (suc b) = 𝒫 R_{1} (b)$
52	50 51	syl	$⊢ b \in ω \to R_{1} (suc b) = 𝒫 R_{1} (b)$
53	52	eleq2d	$⊢ b \in ω \to (c \in R_{1} (suc b) \leftrightarrow c \in 𝒫 R_{1} (b))$
54	53	biimpa	$⊢ (b \in ω \land c \in R_{1} (suc b)) \to c \in 𝒫 R_{1} (b)$
55	54	elpwid	$⊢ (b \in ω \land c \in R_{1} (suc b)) \to c \subseteq R_{1} (b)$
56		resima2	$⊢ c \subseteq R_{1} (b) \to ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) [c] = rec (G, \emptyset) (suc b) [c]$
57	55 56	syl	$⊢ (b \in ω \land c \in R_{1} (suc b)) \to ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) [c] = rec (G, \emptyset) (suc b) [c]$
58	57	fveq2d	$⊢ (b \in ω \land c \in R_{1} (suc b)) \to F (({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) [c]) = F (rec (G, \emptyset) (suc b) [c])$
59		fvex	$⊢ rec (G, \emptyset) (suc b) \in V$
60	59	resex	$⊢ {rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)} \in V$
61		dmeq	$⊢ x = {rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)} \to dom x = dom ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)})$
62	61	pweqd	$⊢ x = {rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)} \to 𝒫 dom x = 𝒫 dom ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)})$
63		imaeq1	$⊢ x = {rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)} \to x [y] = ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) [y]$
64	63	fveq2d	$⊢ x = {rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)} \to F (x [y]) = F (({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) [y])$
65	62 64	mpteq12dv	$⊢ x = {rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)} \to (y \in 𝒫 dom x ⟼ F (x [y])) = (y \in 𝒫 dom ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) ⟼ F (({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) [y]))$
66	60	dmex	$⊢ dom ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) \in V$
67	66	pwex	$⊢ 𝒫 dom ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) \in V$
68	67	mptex	$⊢ (y \in 𝒫 dom ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) ⟼ F (({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) [y])) \in V$
69	65 2 68	fvmpt	$⊢ {rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)} \in V \to G ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) = (y \in 𝒫 dom ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) ⟼ F (({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) [y]))$
70	60 69	ax-mp	$⊢ G ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) = (y \in 𝒫 dom ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) ⟼ F (({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) [y]))$
71	70	fveq1i	$⊢ G ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) (c) = (y \in 𝒫 dom ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) ⟼ F (({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) [y])) (c)$
72		r1sssuc	$⊢ b \in On \to R_{1} (b) \subseteq R_{1} (suc b)$
73	50 72	syl	$⊢ b \in ω \to R_{1} (b) \subseteq R_{1} (suc b)$
74		fnssres	$⊢ (rec (G, \emptyset) (suc b) Fn R_{1} (suc b) \land R_{1} (b) \subseteq R_{1} (suc b)) \to ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) Fn R_{1} (b)$
75	37 73 74	syl2anc	$⊢ b \in ω \to ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) Fn R_{1} (b)$
76	75	fndmd	$⊢ b \in ω \to dom ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) = R_{1} (b)$
77	76	pweqd	$⊢ b \in ω \to 𝒫 dom ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) = 𝒫 R_{1} (b)$
78	77	adantr	$⊢ (b \in ω \land c \in R_{1} (suc b)) \to 𝒫 dom ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) = 𝒫 R_{1} (b)$
79	54 78	eleqtrrd	$⊢ (b \in ω \land c \in R_{1} (suc b)) \to c \in 𝒫 dom ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)})$
80		imaeq2	$⊢ y = c \to ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) [y] = ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) [c]$
81	80	fveq2d	$⊢ y = c \to F (({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) [y]) = F (({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) [c])$
82		eqid	$⊢ (y \in 𝒫 dom ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) ⟼ F (({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) [y])) = (y \in 𝒫 dom ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) ⟼ F (({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) [y]))$
83		fvex	$⊢ F (({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) [c]) \in V$
84	81 82 83	fvmpt	$⊢ c \in 𝒫 dom ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) \to (y \in 𝒫 dom ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) ⟼ F (({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) [y])) (c) = F (({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) [c])$
85	79 84	syl	$⊢ (b \in ω \land c \in R_{1} (suc b)) \to (y \in 𝒫 dom ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) ⟼ F (({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) [y])) (c) = F (({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) [c])$
86	71 85	eqtrid	$⊢ (b \in ω \land c \in R_{1} (suc b)) \to G ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) (c) = F (({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) [c])$
87		dmeq	$⊢ x = rec (G, \emptyset) (suc b) \to dom x = dom rec (G, \emptyset) (suc b)$
88	87	pweqd	$⊢ x = rec (G, \emptyset) (suc b) \to 𝒫 dom x = 𝒫 dom rec (G, \emptyset) (suc b)$
89		imaeq1	$⊢ x = rec (G, \emptyset) (suc b) \to x [y] = rec (G, \emptyset) (suc b) [y]$
90	89	fveq2d	$⊢ x = rec (G, \emptyset) (suc b) \to F (x [y]) = F (rec (G, \emptyset) (suc b) [y])$
91	88 90	mpteq12dv	$⊢ x = rec (G, \emptyset) (suc b) \to (y \in 𝒫 dom x ⟼ F (x [y])) = (y \in 𝒫 dom rec (G, \emptyset) (suc b) ⟼ F (rec (G, \emptyset) (suc b) [y]))$
92	59	dmex	$⊢ dom rec (G, \emptyset) (suc b) \in V$
93	92	pwex	$⊢ 𝒫 dom rec (G, \emptyset) (suc b) \in V$
94	93	mptex	$⊢ (y \in 𝒫 dom rec (G, \emptyset) (suc b) ⟼ F (rec (G, \emptyset) (suc b) [y])) \in V$
95	91 2 94	fvmpt	$⊢ rec (G, \emptyset) (suc b) \in V \to G (rec (G, \emptyset) (suc b)) = (y \in 𝒫 dom rec (G, \emptyset) (suc b) ⟼ F (rec (G, \emptyset) (suc b) [y]))$
96	59 95	ax-mp	$⊢ G (rec (G, \emptyset) (suc b)) = (y \in 𝒫 dom rec (G, \emptyset) (suc b) ⟼ F (rec (G, \emptyset) (suc b) [y]))$
97	96	fveq1i	$⊢ G (rec (G, \emptyset) (suc b)) (c) = (y \in 𝒫 dom rec (G, \emptyset) (suc b) ⟼ F (rec (G, \emptyset) (suc b) [y])) (c)$
98		r1tr	$⊢ Tr R_{1} (suc b)$
99	98	a1i	$⊢ b \in ω \to Tr R_{1} (suc b)$
100		dftr4	$⊢ Tr R_{1} (suc b) \leftrightarrow R_{1} (suc b) \subseteq 𝒫 R_{1} (suc b)$
101	99 100	sylib	$⊢ b \in ω \to R_{1} (suc b) \subseteq 𝒫 R_{1} (suc b)$
102	101	sselda	$⊢ (b \in ω \land c \in R_{1} (suc b)) \to c \in 𝒫 R_{1} (suc b)$
103		f1odm	$⊢ rec (G, \emptyset) (suc b) : R_{1} (suc b) \underset{1-1 onto}{⟶} card (R_{1} (suc b)) \to dom rec (G, \emptyset) (suc b) = R_{1} (suc b)$
104	35 103	syl	$⊢ b \in ω \to dom rec (G, \emptyset) (suc b) = R_{1} (suc b)$
105	104	pweqd	$⊢ b \in ω \to 𝒫 dom rec (G, \emptyset) (suc b) = 𝒫 R_{1} (suc b)$
106	105	adantr	$⊢ (b \in ω \land c \in R_{1} (suc b)) \to 𝒫 dom rec (G, \emptyset) (suc b) = 𝒫 R_{1} (suc b)$
107	102 106	eleqtrrd	$⊢ (b \in ω \land c \in R_{1} (suc b)) \to c \in 𝒫 dom rec (G, \emptyset) (suc b)$
108		imaeq2	$⊢ y = c \to rec (G, \emptyset) (suc b) [y] = rec (G, \emptyset) (suc b) [c]$
109	108	fveq2d	$⊢ y = c \to F (rec (G, \emptyset) (suc b) [y]) = F (rec (G, \emptyset) (suc b) [c])$
110		eqid	$⊢ (y \in 𝒫 dom rec (G, \emptyset) (suc b) ⟼ F (rec (G, \emptyset) (suc b) [y])) = (y \in 𝒫 dom rec (G, \emptyset) (suc b) ⟼ F (rec (G, \emptyset) (suc b) [y]))$
111		fvex	$⊢ F (rec (G, \emptyset) (suc b) [c]) \in V$
112	109 110 111	fvmpt	$⊢ c \in 𝒫 dom rec (G, \emptyset) (suc b) \to (y \in 𝒫 dom rec (G, \emptyset) (suc b) ⟼ F (rec (G, \emptyset) (suc b) [y])) (c) = F (rec (G, \emptyset) (suc b) [c])$
113	107 112	syl	$⊢ (b \in ω \land c \in R_{1} (suc b)) \to (y \in 𝒫 dom rec (G, \emptyset) (suc b) ⟼ F (rec (G, \emptyset) (suc b) [y])) (c) = F (rec (G, \emptyset) (suc b) [c])$
114	97 113	eqtrid	$⊢ (b \in ω \land c \in R_{1} (suc b)) \to G (rec (G, \emptyset) (suc b)) (c) = F (rec (G, \emptyset) (suc b) [c])$
115	58 86 114	3eqtr4d	$⊢ (b \in ω \land c \in R_{1} (suc b)) \to G ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) (c) = G (rec (G, \emptyset) (suc b)) (c)$
116	115	adantlr	$⊢ ((b \in ω \land rec (G, \emptyset) (b) = {rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) \land c \in R_{1} (suc b)) \to G ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) (c) = G (rec (G, \emptyset) (suc b)) (c)$
117		fveq2	$⊢ rec (G, \emptyset) (b) = {rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)} \to G (rec (G, \emptyset) (b)) = G ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)})$
118	117	fveq1d	$⊢ rec (G, \emptyset) (b) = {rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)} \to G (rec (G, \emptyset) (b)) (c) = G ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) (c)$
119	118	ad2antlr	$⊢ ((b \in ω \land rec (G, \emptyset) (b) = {rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) \land c \in R_{1} (suc b)) \to G (rec (G, \emptyset) (b)) (c) = G ({rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) (c)$
120		rdgsuc	$⊢ suc b \in On \to rec (G, \emptyset) (suc suc b) = G (rec (G, \emptyset) (suc b))$
121	44 120	syl	$⊢ b \in ω \to rec (G, \emptyset) (suc suc b) = G (rec (G, \emptyset) (suc b))$
122	121	fveq1d	$⊢ b \in ω \to rec (G, \emptyset) (suc suc b) (c) = G (rec (G, \emptyset) (suc b)) (c)$
123	122	ad2antrr	$⊢ ((b \in ω \land rec (G, \emptyset) (b) = {rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) \land c \in R_{1} (suc b)) \to rec (G, \emptyset) (suc suc b) (c) = G (rec (G, \emptyset) (suc b)) (c)$
124	116 119 123	3eqtr4rd	$⊢ ((b \in ω \land rec (G, \emptyset) (b) = {rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) \land c \in R_{1} (suc b)) \to rec (G, \emptyset) (suc suc b) (c) = G (rec (G, \emptyset) (b)) (c)$
125		fvres	$⊢ c \in R_{1} (suc b) \to ({rec (G, \emptyset) (suc suc b) ↾}_{R_{1} (suc b)}) (c) = rec (G, \emptyset) (suc suc b) (c)$
126	125	adantl	$⊢ ((b \in ω \land rec (G, \emptyset) (b) = {rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) \land c \in R_{1} (suc b)) \to ({rec (G, \emptyset) (suc suc b) ↾}_{R_{1} (suc b)}) (c) = rec (G, \emptyset) (suc suc b) (c)$
127		rdgsuc	$⊢ b \in On \to rec (G, \emptyset) (suc b) = G (rec (G, \emptyset) (b))$
128	50 127	syl	$⊢ b \in ω \to rec (G, \emptyset) (suc b) = G (rec (G, \emptyset) (b))$
129	128	fveq1d	$⊢ b \in ω \to rec (G, \emptyset) (suc b) (c) = G (rec (G, \emptyset) (b)) (c)$
130	129	ad2antrr	$⊢ ((b \in ω \land rec (G, \emptyset) (b) = {rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) \land c \in R_{1} (suc b)) \to rec (G, \emptyset) (suc b) (c) = G (rec (G, \emptyset) (b)) (c)$
131	124 126 130	3eqtr4rd	$⊢ ((b \in ω \land rec (G, \emptyset) (b) = {rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) \land c \in R_{1} (suc b)) \to rec (G, \emptyset) (suc b) (c) = ({rec (G, \emptyset) (suc suc b) ↾}_{R_{1} (suc b)}) (c)$
132	38 49 131	eqfnfvd	$⊢ (b \in ω \land rec (G, \emptyset) (b) = {rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)}) \to rec (G, \emptyset) (suc b) = {rec (G, \emptyset) (suc suc b) ↾}_{R_{1} (suc b)}$
133	132	ex	$⊢ b \in ω \to (rec (G, \emptyset) (b) = {rec (G, \emptyset) (suc b) ↾}_{R_{1} (b)} \to rec (G, \emptyset) (suc b) = {rec (G, \emptyset) (suc suc b) ↾}_{R_{1} (suc b)})$
134	8 14 20 26 32 133	finds	$⊢ A \in ω \to rec (G, \emptyset) (A) = {rec (G, \emptyset) (suc A) ↾}_{R_{1} (A)}$
135		resss	$⊢ {rec (G, \emptyset) (suc A) ↾}_{R_{1} (A)} \subseteq rec (G, \emptyset) (suc A)$
136	134 135	eqsstrdi	$⊢ A \in ω \to rec (G, \emptyset) (A) \subseteq rec (G, \emptyset) (suc A)$

Metamath Proof Explorer

Theorem ackbij2lem3

Proof