Theorem ackbij2lem3 10006

Description: Lemma for ackbij2 10008. (Contributed by Stefan O'Rear, 18-Nov-2014.)

Hypotheses

Ref	Expression
ackbij.f	⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))
ackbij.g	⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))))

Assertion

Ref	Expression
ackbij2lem3	⊢ (𝐴 ∈ ω → (rec(𝐺, ∅)‘𝐴) ⊆ (rec(𝐺, ∅)‘suc 𝐴))

Distinct variable groups:   𝑥,𝐹,𝑦   𝑥,𝐺,𝑦   𝑥,𝐴,𝑦

Proof of Theorem ackbij2lem3

Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6783	. . . 4 ⊢ (𝑎 = ∅ → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘∅))
2		suceq 6335	. . . . . 6 ⊢ (𝑎 = ∅ → suc 𝑎 = suc ∅)
3	2	fveq2d 6787	. . . . 5 ⊢ (𝑎 = ∅ → (rec(𝐺, ∅)‘suc 𝑎) = (rec(𝐺, ∅)‘suc ∅))
4		fveq2 6783	. . . . 5 ⊢ (𝑎 = ∅ → (𝑅1‘𝑎) = (𝑅1‘∅))
5	3, 4	reseq12d 5895	. . . 4 ⊢ (𝑎 = ∅ → ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) = ((rec(𝐺, ∅)‘suc ∅) ↾ (𝑅1‘∅)))
6	1, 5	eqeq12d 2755	. . 3 ⊢ (𝑎 = ∅ → ((rec(𝐺, ∅)‘𝑎) = ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) ↔ (rec(𝐺, ∅)‘∅) = ((rec(𝐺, ∅)‘suc ∅) ↾ (𝑅1‘∅))))
7		fveq2 6783	. . . 4 ⊢ (𝑎 = 𝑏 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘𝑏))
8		suceq 6335	. . . . . 6 ⊢ (𝑎 = 𝑏 → suc 𝑎 = suc 𝑏)
9	8	fveq2d 6787	. . . . 5 ⊢ (𝑎 = 𝑏 → (rec(𝐺, ∅)‘suc 𝑎) = (rec(𝐺, ∅)‘suc 𝑏))
10		fveq2 6783	. . . . 5 ⊢ (𝑎 = 𝑏 → (𝑅1‘𝑎) = (𝑅1‘𝑏))
11	9, 10	reseq12d 5895	. . . 4 ⊢ (𝑎 = 𝑏 → ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))
12	7, 11	eqeq12d 2755	. . 3 ⊢ (𝑎 = 𝑏 → ((rec(𝐺, ∅)‘𝑎) = ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) ↔ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))))
13		fveq2 6783	. . . 4 ⊢ (𝑎 = suc 𝑏 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘suc 𝑏))
14		suceq 6335	. . . . . 6 ⊢ (𝑎 = suc 𝑏 → suc 𝑎 = suc suc 𝑏)
15	14	fveq2d 6787	. . . . 5 ⊢ (𝑎 = suc 𝑏 → (rec(𝐺, ∅)‘suc 𝑎) = (rec(𝐺, ∅)‘suc suc 𝑏))
16		fveq2 6783	. . . . 5 ⊢ (𝑎 = suc 𝑏 → (𝑅1‘𝑎) = (𝑅1‘suc 𝑏))
17	15, 16	reseq12d 5895	. . . 4 ⊢ (𝑎 = suc 𝑏 → ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) = ((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏)))
18	13, 17	eqeq12d 2755	. . 3 ⊢ (𝑎 = suc 𝑏 → ((rec(𝐺, ∅)‘𝑎) = ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) ↔ (rec(𝐺, ∅)‘suc 𝑏) = ((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏))))
19		fveq2 6783	. . . 4 ⊢ (𝑎 = 𝐴 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘𝐴))
20		suceq 6335	. . . . . 6 ⊢ (𝑎 = 𝐴 → suc 𝑎 = suc 𝐴)
21	20	fveq2d 6787	. . . . 5 ⊢ (𝑎 = 𝐴 → (rec(𝐺, ∅)‘suc 𝑎) = (rec(𝐺, ∅)‘suc 𝐴))
22		fveq2 6783	. . . . 5 ⊢ (𝑎 = 𝐴 → (𝑅1‘𝑎) = (𝑅1‘𝐴))
23	21, 22	reseq12d 5895	. . . 4 ⊢ (𝑎 = 𝐴 → ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) = ((rec(𝐺, ∅)‘suc 𝐴) ↾ (𝑅1‘𝐴)))
24	19, 23	eqeq12d 2755	. . 3 ⊢ (𝑎 = 𝐴 → ((rec(𝐺, ∅)‘𝑎) = ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) ↔ (rec(𝐺, ∅)‘𝐴) = ((rec(𝐺, ∅)‘suc 𝐴) ↾ (𝑅1‘𝐴))))
25		res0 5898	. . . 4 ⊢ ((rec(𝐺, ∅)‘suc ∅) ↾ ∅) = ∅
26		r10 9535	. . . . 5 ⊢ (𝑅1‘∅) = ∅
27	26	reseq2i 5891	. . . 4 ⊢ ((rec(𝐺, ∅)‘suc ∅) ↾ (𝑅1‘∅)) = ((rec(𝐺, ∅)‘suc ∅) ↾ ∅)
28		0ex 5232	. . . . 5 ⊢ ∅ ∈ V
29	28	rdg0 8261	. . . 4 ⊢ (rec(𝐺, ∅)‘∅) = ∅
30	25, 27, 29	3eqtr4ri 2778	. . 3 ⊢ (rec(𝐺, ∅)‘∅) = ((rec(𝐺, ∅)‘suc ∅) ↾ (𝑅1‘∅))
31		peano2 7746	. . . . . . . 8 ⊢ (𝑏 ∈ ω → suc 𝑏 ∈ ω)
32		ackbij.f	. . . . . . . . 9 ⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))
33		ackbij.g	. . . . . . . . 9 ⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))))
34	32, 33	ackbij2lem2 10005	. . . . . . . 8 ⊢ (suc 𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏)))
35	31, 34	syl 17	. . . . . . 7 ⊢ (𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏)))
36		f1ofn 6726	. . . . . . 7 ⊢ ((rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏)) → (rec(𝐺, ∅)‘suc 𝑏) Fn (𝑅1‘suc 𝑏))
37	35, 36	syl 17	. . . . . 6 ⊢ (𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏) Fn (𝑅1‘suc 𝑏))
38	37	adantr 481	. . . . 5 ⊢ ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) → (rec(𝐺, ∅)‘suc 𝑏) Fn (𝑅1‘suc 𝑏))
39		peano2 7746	. . . . . . . 8 ⊢ (suc 𝑏 ∈ ω → suc suc 𝑏 ∈ ω)
40	32, 33	ackbij2lem2 10005	. . . . . . . 8 ⊢ (suc suc 𝑏 ∈ ω → (rec(𝐺, ∅)‘suc suc 𝑏):(𝑅1‘suc suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc suc 𝑏)))
41		f1ofn 6726	. . . . . . . 8 ⊢ ((rec(𝐺, ∅)‘suc suc 𝑏):(𝑅1‘suc suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc suc 𝑏)) → (rec(𝐺, ∅)‘suc suc 𝑏) Fn (𝑅1‘suc suc 𝑏))
42	31, 39, 40, 41	4syl 19	. . . . . . 7 ⊢ (𝑏 ∈ ω → (rec(𝐺, ∅)‘suc suc 𝑏) Fn (𝑅1‘suc suc 𝑏))
43		nnon 7727	. . . . . . . . 9 ⊢ (suc 𝑏 ∈ ω → suc 𝑏 ∈ On)
44	31, 43	syl 17	. . . . . . . 8 ⊢ (𝑏 ∈ ω → suc 𝑏 ∈ On)
45		r1sssuc 9550	. . . . . . . 8 ⊢ (suc 𝑏 ∈ On → (𝑅1‘suc 𝑏) ⊆ (𝑅1‘suc suc 𝑏))
46	44, 45	syl 17	. . . . . . 7 ⊢ (𝑏 ∈ ω → (𝑅1‘suc 𝑏) ⊆ (𝑅1‘suc suc 𝑏))
47		fnssres 6564	. . . . . . 7 ⊢ (((rec(𝐺, ∅)‘suc suc 𝑏) Fn (𝑅1‘suc suc 𝑏) ∧ (𝑅1‘suc 𝑏) ⊆ (𝑅1‘suc suc 𝑏)) → ((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏)) Fn (𝑅1‘suc 𝑏))
48	42, 46, 47	syl2anc 584	. . . . . 6 ⊢ (𝑏 ∈ ω → ((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏)) Fn (𝑅1‘suc 𝑏))
49	48	adantr 481	. . . . 5 ⊢ ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) → ((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏)) Fn (𝑅1‘suc 𝑏))
50		nnon 7727	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ ω → 𝑏 ∈ On)
51		r1suc 9537	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ On → (𝑅1‘suc 𝑏) = 𝒫 (𝑅1‘𝑏))
52	50, 51	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ ω → (𝑅1‘suc 𝑏) = 𝒫 (𝑅1‘𝑏))
53	52	eleq2d 2825	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ ω → (𝑐 ∈ (𝑅1‘suc 𝑏) ↔ 𝑐 ∈ 𝒫 (𝑅1‘𝑏)))
54	53	biimpa 477	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝑐 ∈ 𝒫 (𝑅1‘𝑏))
55	54	elpwid 4545	. . . . . . . . . . 11 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝑐 ⊆ (𝑅1‘𝑏))
56		resima2 5929	. . . . . . . . . . 11 ⊢ (𝑐 ⊆ (𝑅1‘𝑏) → (((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐) = ((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐))
57	55, 56	syl 17	. . . . . . . . . 10 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → (((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐) = ((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐))
58	57	fveq2d 6787	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐)) = (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐)))
59		fvex 6796	. . . . . . . . . . . . 13 ⊢ (rec(𝐺, ∅)‘suc 𝑏) ∈ V
60	59	resex 5942	. . . . . . . . . . . 12 ⊢ ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ∈ V
61		dmeq 5815	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → dom 𝑥 = dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))
62	61	pweqd 4553	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → 𝒫 dom 𝑥 = 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))
63		imaeq1 5967	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → (𝑥 “ 𝑦) = (((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦))
64	63	fveq2d 6787	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → (𝐹‘(𝑥 “ 𝑦)) = (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)))
65	62, 64	mpteq12dv 5166	. . . . . . . . . . . . 13 ⊢ (𝑥 = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))) = (𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦))))
66	60	dmex 7767	. . . . . . . . . . . . . . 15 ⊢ dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ∈ V
67	66	pwex 5304	. . . . . . . . . . . . . 14 ⊢ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ∈ V
68	67	mptex 7108	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦))) ∈ V
69	65, 33, 68	fvmpt 6884	. . . . . . . . . . . 12 ⊢ (((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ∈ V → (𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) = (𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦))))
70	60, 69	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) = (𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)))
71	70	fveq1i 6784	. . . . . . . . . 10 ⊢ ((𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))‘𝑐) = ((𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)))‘𝑐)
72		r1sssuc 9550	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ On → (𝑅1‘𝑏) ⊆ (𝑅1‘suc 𝑏))
73	50, 72	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ ω → (𝑅1‘𝑏) ⊆ (𝑅1‘suc 𝑏))
74		fnssres 6564	. . . . . . . . . . . . . . . 16 ⊢ (((rec(𝐺, ∅)‘suc 𝑏) Fn (𝑅1‘suc 𝑏) ∧ (𝑅1‘𝑏) ⊆ (𝑅1‘suc 𝑏)) → ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) Fn (𝑅1‘𝑏))
75	37, 73, 74	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ ω → ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) Fn (𝑅1‘𝑏))
76	75	fndmd 6547	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ ω → dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) = (𝑅1‘𝑏))
77	76	pweqd 4553	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ ω → 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) = 𝒫 (𝑅1‘𝑏))
78	77	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) = 𝒫 (𝑅1‘𝑏))
79	54, 78	eleqtrrd 2843	. . . . . . . . . . 11 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝑐 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))
80		imaeq2 5968	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑐 → (((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦) = (((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐))
81	80	fveq2d 6787	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑐 → (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)) = (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐)))
82		eqid 2739	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦))) = (𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)))
83		fvex 6796	. . . . . . . . . . . 12 ⊢ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐)) ∈ V
84	81, 82, 83	fvmpt 6884	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → ((𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)))‘𝑐) = (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐)))
85	79, 84	syl 17	. . . . . . . . . 10 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)))‘𝑐) = (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐)))
86	71, 85	eqtrid 2791	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))‘𝑐) = (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐)))
87		dmeq 5815	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (rec(𝐺, ∅)‘suc 𝑏) → dom 𝑥 = dom (rec(𝐺, ∅)‘suc 𝑏))
88	87	pweqd 4553	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (rec(𝐺, ∅)‘suc 𝑏) → 𝒫 dom 𝑥 = 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏))
89		imaeq1 5967	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (rec(𝐺, ∅)‘suc 𝑏) → (𝑥 “ 𝑦) = ((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦))
90	89	fveq2d 6787	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (rec(𝐺, ∅)‘suc 𝑏) → (𝐹‘(𝑥 “ 𝑦)) = (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)))
91	88, 90	mpteq12dv 5166	. . . . . . . . . . . . 13 ⊢ (𝑥 = (rec(𝐺, ∅)‘suc 𝑏) → (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦))))
92	59	dmex 7767	. . . . . . . . . . . . . . 15 ⊢ dom (rec(𝐺, ∅)‘suc 𝑏) ∈ V
93	92	pwex 5304	. . . . . . . . . . . . . 14 ⊢ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ∈ V
94	93	mptex 7108	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦))) ∈ V
95	91, 33, 94	fvmpt 6884	. . . . . . . . . . . 12 ⊢ ((rec(𝐺, ∅)‘suc 𝑏) ∈ V → (𝐺‘(rec(𝐺, ∅)‘suc 𝑏)) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦))))
96	59, 95	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝐺‘(rec(𝐺, ∅)‘suc 𝑏)) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)))
97	96	fveq1i 6784	. . . . . . . . . 10 ⊢ ((𝐺‘(rec(𝐺, ∅)‘suc 𝑏))‘𝑐) = ((𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)))‘𝑐)
98		r1tr 9543	. . . . . . . . . . . . . . 15 ⊢ Tr (𝑅1‘suc 𝑏)
99	98	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ ω → Tr (𝑅1‘suc 𝑏))
100		dftr4 5197	. . . . . . . . . . . . . 14 ⊢ (Tr (𝑅1‘suc 𝑏) ↔ (𝑅1‘suc 𝑏) ⊆ 𝒫 (𝑅1‘suc 𝑏))
101	99, 100	sylib 217	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ ω → (𝑅1‘suc 𝑏) ⊆ 𝒫 (𝑅1‘suc 𝑏))
102	101	sselda 3922	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝑐 ∈ 𝒫 (𝑅1‘suc 𝑏))
103		f1odm 6729	. . . . . . . . . . . . . . 15 ⊢ ((rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏)) → dom (rec(𝐺, ∅)‘suc 𝑏) = (𝑅1‘suc 𝑏))
104	35, 103	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ ω → dom (rec(𝐺, ∅)‘suc 𝑏) = (𝑅1‘suc 𝑏))
105	104	pweqd 4553	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ ω → 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) = 𝒫 (𝑅1‘suc 𝑏))
106	105	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) = 𝒫 (𝑅1‘suc 𝑏))
107	102, 106	eleqtrrd 2843	. . . . . . . . . . 11 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝑐 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏))
108		imaeq2 5968	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑐 → ((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦) = ((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐))
109	108	fveq2d 6787	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑐 → (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)) = (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐)))
110		eqid 2739	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦))) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)))
111		fvex 6796	. . . . . . . . . . . 12 ⊢ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐)) ∈ V
112	109, 110, 111	fvmpt 6884	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) → ((𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)))‘𝑐) = (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐)))
113	107, 112	syl 17	. . . . . . . . . 10 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)))‘𝑐) = (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐)))
114	97, 113	eqtrid 2791	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((𝐺‘(rec(𝐺, ∅)‘suc 𝑏))‘𝑐) = (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐)))
115	58, 86, 114	3eqtr4d 2789	. . . . . . . 8 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘suc 𝑏))‘𝑐))
116	115	adantlr 712	. . . . . . 7 ⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘suc 𝑏))‘𝑐))
117		fveq2 6783	. . . . . . . . 9 ⊢ ((rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → (𝐺‘(rec(𝐺, ∅)‘𝑏)) = (𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))))
118	117	fveq1d 6785	. . . . . . . 8 ⊢ ((rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → ((𝐺‘(rec(𝐺, ∅)‘𝑏))‘𝑐) = ((𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))‘𝑐))
119	118	ad2antlr 724	. . . . . . 7 ⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((𝐺‘(rec(𝐺, ∅)‘𝑏))‘𝑐) = ((𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))‘𝑐))
120		rdgsuc 8264	. . . . . . . . . 10 ⊢ (suc 𝑏 ∈ On → (rec(𝐺, ∅)‘suc suc 𝑏) = (𝐺‘(rec(𝐺, ∅)‘suc 𝑏)))
121	44, 120	syl 17	. . . . . . . . 9 ⊢ (𝑏 ∈ ω → (rec(𝐺, ∅)‘suc suc 𝑏) = (𝐺‘(rec(𝐺, ∅)‘suc 𝑏)))
122	121	fveq1d 6785	. . . . . . . 8 ⊢ (𝑏 ∈ ω → ((rec(𝐺, ∅)‘suc suc 𝑏)‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘suc 𝑏))‘𝑐))
123	122	ad2antrr 723	. . . . . . 7 ⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((rec(𝐺, ∅)‘suc suc 𝑏)‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘suc 𝑏))‘𝑐))
124	116, 119, 123	3eqtr4rd 2790	. . . . . 6 ⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((rec(𝐺, ∅)‘suc suc 𝑏)‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘𝑏))‘𝑐))
125		fvres 6802	. . . . . . 7 ⊢ (𝑐 ∈ (𝑅1‘suc 𝑏) → (((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏))‘𝑐) = ((rec(𝐺, ∅)‘suc suc 𝑏)‘𝑐))
126	125	adantl 482	. . . . . 6 ⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → (((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏))‘𝑐) = ((rec(𝐺, ∅)‘suc suc 𝑏)‘𝑐))
127		rdgsuc 8264	. . . . . . . . 9 ⊢ (𝑏 ∈ On → (rec(𝐺, ∅)‘suc 𝑏) = (𝐺‘(rec(𝐺, ∅)‘𝑏)))
128	50, 127	syl 17	. . . . . . . 8 ⊢ (𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏) = (𝐺‘(rec(𝐺, ∅)‘𝑏)))
129	128	fveq1d 6785	. . . . . . 7 ⊢ (𝑏 ∈ ω → ((rec(𝐺, ∅)‘suc 𝑏)‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘𝑏))‘𝑐))
130	129	ad2antrr 723	. . . . . 6 ⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((rec(𝐺, ∅)‘suc 𝑏)‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘𝑏))‘𝑐))
131	124, 126, 130	3eqtr4rd 2790	. . . . 5 ⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((rec(𝐺, ∅)‘suc 𝑏)‘𝑐) = (((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏))‘𝑐))
132	38, 49, 131	eqfnfvd 6921	. . . 4 ⊢ ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) → (rec(𝐺, ∅)‘suc 𝑏) = ((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏)))
133	132	ex 413	. . 3 ⊢ (𝑏 ∈ ω → ((rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → (rec(𝐺, ∅)‘suc 𝑏) = ((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏))))
134	6, 12, 18, 24, 30, 133	finds 7754	. 2 ⊢ (𝐴 ∈ ω → (rec(𝐺, ∅)‘𝐴) = ((rec(𝐺, ∅)‘suc 𝐴) ↾ (𝑅1‘𝐴)))
135		resss 5919	. 2 ⊢ ((rec(𝐺, ∅)‘suc 𝐴) ↾ (𝑅1‘𝐴)) ⊆ (rec(𝐺, ∅)‘suc 𝐴)
136	134, 135	eqsstrdi 3976	1 ⊢ (𝐴 ∈ ω → (rec(𝐺, ∅)‘𝐴) ⊆ (rec(𝐺, ∅)‘suc 𝐴))

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2107  Vcvv 3433   ∩ cin 3887   ⊆ wss 3888  ∅c0 4257  𝒫 cpw 4534  {csn 4562  ∪ ciun 4925   ↦ cmpt 5158  Tr wtr 5192   × cxp 5588  dom cdm 5590   ↾ cres 5592   “ cima 5593  Oncon0 6270  suc csuc 6272   Fn wfn 6432  –1-1-onto→wf1o 6436  ‘cfv 6437  ωcom 7721  reccrdg 8249  Fincfn 8742  𝑅₁cr1 9529  cardccrd 9702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-int 4881  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-ov 7287  df-oprab 7288  df-mpo 7289  df-om 7722  df-1st 7840  df-2nd 7841  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-1o 8306  df-2o 8307  df-oadd 8310  df-er 8507  df-map 8626  df-en 8743  df-dom 8744  df-sdom 8745  df-fin 8746  df-r1 9531  df-dju 9668  df-card 9706

This theorem is referenced by:  ackbij2lem4  10007