Theorem ackbij2lem3 10311

Description: Lemma for ackbij2 10313. (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 6883	. . . 4 ⊢ (𝑎 = ∅ → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘∅))
2		suceq 6430	. . . . . 6 ⊢ (𝑎 = ∅ → suc 𝑎 = suc ∅)
3	2	fveq2d 6887	. . . . 5 ⊢ (𝑎 = ∅ → (rec(𝐺, ∅)‘suc 𝑎) = (rec(𝐺, ∅)‘suc ∅))
4		fveq2 6883	. . . . 5 ⊢ (𝑎 = ∅ → (𝑅1‘𝑎) = (𝑅1‘∅))
5	3, 4	reseq12d 5971	. . . 4 ⊢ (𝑎 = ∅ → ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) = ((rec(𝐺, ∅)‘suc ∅) ↾ (𝑅1‘∅)))
6	1, 5	eqeq12d 2777	. . 3 ⊢ (𝑎 = ∅ → ((rec(𝐺, ∅)‘𝑎) = ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) ↔ (rec(𝐺, ∅)‘∅) = ((rec(𝐺, ∅)‘suc ∅) ↾ (𝑅1‘∅))))
7		fveq2 6883	. . . 4 ⊢ (𝑎 = 𝑏 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘𝑏))
8		suceq 6430	. . . . . 6 ⊢ (𝑎 = 𝑏 → suc 𝑎 = suc 𝑏)
9	8	fveq2d 6887	. . . . 5 ⊢ (𝑎 = 𝑏 → (rec(𝐺, ∅)‘suc 𝑎) = (rec(𝐺, ∅)‘suc 𝑏))
10		fveq2 6883	. . . . 5 ⊢ (𝑎 = 𝑏 → (𝑅1‘𝑎) = (𝑅1‘𝑏))
11	9, 10	reseq12d 5971	. . . 4 ⊢ (𝑎 = 𝑏 → ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))
12	7, 11	eqeq12d 2777	. . 3 ⊢ (𝑎 = 𝑏 → ((rec(𝐺, ∅)‘𝑎) = ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) ↔ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))))
13		fveq2 6883	. . . 4 ⊢ (𝑎 = suc 𝑏 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘suc 𝑏))
14		suceq 6430	. . . . . 6 ⊢ (𝑎 = suc 𝑏 → suc 𝑎 = suc suc 𝑏)
15	14	fveq2d 6887	. . . . 5 ⊢ (𝑎 = suc 𝑏 → (rec(𝐺, ∅)‘suc 𝑎) = (rec(𝐺, ∅)‘suc suc 𝑏))
16		fveq2 6883	. . . . 5 ⊢ (𝑎 = suc 𝑏 → (𝑅1‘𝑎) = (𝑅1‘suc 𝑏))
17	15, 16	reseq12d 5971	. . . 4 ⊢ (𝑎 = suc 𝑏 → ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) = ((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏)))
18	13, 17	eqeq12d 2777	. . 3 ⊢ (𝑎 = suc 𝑏 → ((rec(𝐺, ∅)‘𝑎) = ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) ↔ (rec(𝐺, ∅)‘suc 𝑏) = ((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏))))
19		fveq2 6883	. . . 4 ⊢ (𝑎 = 𝐴 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘𝐴))
20		suceq 6430	. . . . . 6 ⊢ (𝑎 = 𝐴 → suc 𝑎 = suc 𝐴)
21	20	fveq2d 6887	. . . . 5 ⊢ (𝑎 = 𝐴 → (rec(𝐺, ∅)‘suc 𝑎) = (rec(𝐺, ∅)‘suc 𝐴))
22		fveq2 6883	. . . . 5 ⊢ (𝑎 = 𝐴 → (𝑅1‘𝑎) = (𝑅1‘𝐴))
23	21, 22	reseq12d 5971	. . . 4 ⊢ (𝑎 = 𝐴 → ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) = ((rec(𝐺, ∅)‘suc 𝐴) ↾ (𝑅1‘𝐴)))
24	19, 23	eqeq12d 2777	. . 3 ⊢ (𝑎 = 𝐴 → ((rec(𝐺, ∅)‘𝑎) = ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) ↔ (rec(𝐺, ∅)‘𝐴) = ((rec(𝐺, ∅)‘suc 𝐴) ↾ (𝑅1‘𝐴))))
25		res0 5974	. . . 4 ⊢ ((rec(𝐺, ∅)‘suc ∅) ↾ ∅) = ∅
26		r10 9768	. . . . 5 ⊢ (𝑅1‘∅) = ∅
27	26	reseq2i 5967	. . . 4 ⊢ ((rec(𝐺, ∅)‘suc ∅) ↾ (𝑅1‘∅)) = ((rec(𝐺, ∅)‘suc ∅) ↾ ∅)
28		0ex 5261	. . . . 5 ⊢ ∅ ∈ V
29	28	rdg0 8422	. . . 4 ⊢ (rec(𝐺, ∅)‘∅) = ∅
30	25, 27, 29	3eqtr4ri 2795	. . 3 ⊢ (rec(𝐺, ∅)‘∅) = ((rec(𝐺, ∅)‘suc ∅) ↾ (𝑅1‘∅))
31		peano2 7899	. . . . . . . 8 ⊢ (𝑏 ∈ ω → suc 𝑏 ∈ ω)
32		ackbij.f	. . . . . . . . 9 ⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))
33		ackbij.g	. . . . . . . . 9 ⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))))
34	32, 33	ackbij2lem2 10310	. . . . . . . 8 ⊢ (suc 𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏)))
35	31, 34	syl 18	. . . . . . 7 ⊢ (𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏)))
36		f1ofn 6823	. . . . . . 7 ⊢ ((rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏)) → (rec(𝐺, ∅)‘suc 𝑏) Fn (𝑅1‘suc 𝑏))
37	35, 36	syl 18	. . . . . 6 ⊢ (𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏) Fn (𝑅1‘suc 𝑏))
38	37	adantr 486	. . . . 5 ⊢ ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) → (rec(𝐺, ∅)‘suc 𝑏) Fn (𝑅1‘suc 𝑏))
39		peano2 7899	. . . . . . . 8 ⊢ (suc 𝑏 ∈ ω → suc suc 𝑏 ∈ ω)
40	32, 33	ackbij2lem2 10310	. . . . . . . 8 ⊢ (suc suc 𝑏 ∈ ω → (rec(𝐺, ∅)‘suc suc 𝑏):(𝑅1‘suc suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc suc 𝑏)))
41		f1ofn 6823	. . . . . . . 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 20	. . . . . . 7 ⊢ (𝑏 ∈ ω → (rec(𝐺, ∅)‘suc suc 𝑏) Fn (𝑅1‘suc suc 𝑏))
43		nnon 7881	. . . . . . . . 9 ⊢ (suc 𝑏 ∈ ω → suc 𝑏 ∈ On)
44	31, 43	syl 18	. . . . . . . 8 ⊢ (𝑏 ∈ ω → suc 𝑏 ∈ On)
45		r1sssuc 9783	. . . . . . . 8 ⊢ (suc 𝑏 ∈ On → (𝑅1‘suc 𝑏) ⊆ (𝑅1‘suc suc 𝑏))
46	44, 45	syl 18	. . . . . . 7 ⊢ (𝑏 ∈ ω → (𝑅1‘suc 𝑏) ⊆ (𝑅1‘suc suc 𝑏))
47		fnssres 6660	. . . . . . 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 596	. . . . . 6 ⊢ (𝑏 ∈ ω → ((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏)) Fn (𝑅1‘suc 𝑏))
49	48	adantr 486	. . . . 5 ⊢ ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) → ((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏)) Fn (𝑅1‘suc 𝑏))
50		nnon 7881	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ ω → 𝑏 ∈ On)
51		r1suc 9770	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ On → (𝑅1‘suc 𝑏) = 𝒫 (𝑅1‘𝑏))
52	50, 51	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ ω → (𝑅1‘suc 𝑏) = 𝒫 (𝑅1‘𝑏))
53	52	eleq2d 2847	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ ω → (𝑐 ∈ (𝑅1‘suc 𝑏) ↔ 𝑐 ∈ 𝒫 (𝑅1‘𝑏)))
54	53	biimpa 482	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝑐 ∈ 𝒫 (𝑅1‘𝑏))
55	54	elpwid 4566	. . . . . . . . . . 11 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝑐 ⊆ (𝑅1‘𝑏))
56		resima2 6057	. . . . . . . . . . 11 ⊢ (𝑐 ⊆ (𝑅1‘𝑏) → (((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐) = ((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐))
57	55, 56	syl 18	. . . . . . . . . 10 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → (((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐) = ((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐))
58	57	fveq2d 6887	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐)) = (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐)))
59		fvex 6896	. . . . . . . . . . . . 13 ⊢ (rec(𝐺, ∅)‘suc 𝑏) ∈ V
60	59	resex 6018	. . . . . . . . . . . 12 ⊢ ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ∈ V
61		dmeq 5885	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → dom 𝑥 = dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))
62	61	pweqd 4574	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → 𝒫 dom 𝑥 = 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))
63		imaeq1 6047	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → (𝑥 “ 𝑦) = (((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦))
64	63	fveq2d 6887	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → (𝐹‘(𝑥 “ 𝑦)) = (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)))
65	62, 64	mpteq12dv 5192	. . . . . . . . . . . . 13 ⊢ (𝑥 = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))) = (𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦))))
66	60	dmex 7919	. . . . . . . . . . . . . . 15 ⊢ dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ∈ V
67	66	pwex 5342	. . . . . . . . . . . . . 14 ⊢ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ∈ V
68	67	mptex 7227	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦))) ∈ V
69	65, 33, 68	fvmpt 6991	. . . . . . . . . . . 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 6884	. . . . . . . . . 10 ⊢ ((𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))‘𝑐) = ((𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)))‘𝑐)
72		r1sssuc 9783	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ On → (𝑅1‘𝑏) ⊆ (𝑅1‘suc 𝑏))
73	50, 72	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ ω → (𝑅1‘𝑏) ⊆ (𝑅1‘suc 𝑏))
74		fnssres 6660	. . . . . . . . . . . . . . . 16 ⊢ (((rec(𝐺, ∅)‘suc 𝑏) Fn (𝑅1‘suc 𝑏) ∧ (𝑅1‘𝑏) ⊆ (𝑅1‘suc 𝑏)) → ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) Fn (𝑅1‘𝑏))
75	37, 73, 74	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ ω → ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) Fn (𝑅1‘𝑏))
76	75	fndmd 6642	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ ω → dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) = (𝑅1‘𝑏))
77	76	pweqd 4574	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ ω → 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) = 𝒫 (𝑅1‘𝑏))
78	77	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) = 𝒫 (𝑅1‘𝑏))
79	54, 78	eleqtrrd 2864	. . . . . . . . . . 11 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝑐 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))
80		imaeq2 6048	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑐 → (((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦) = (((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐))
81	80	fveq2d 6887	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑐 → (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)) = (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐)))
82		eqid 2761	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦))) = (𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)))
83		fvex 6896	. . . . . . . . . . . 12 ⊢ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐)) ∈ V
84	81, 82, 83	fvmpt 6991	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → ((𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)))‘𝑐) = (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐)))
85	79, 84	syl 18	. . . . . . . . . 10 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)))‘𝑐) = (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐)))
86	71, 85	eqtrid 2808	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))‘𝑐) = (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐)))
87		dmeq 5885	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (rec(𝐺, ∅)‘suc 𝑏) → dom 𝑥 = dom (rec(𝐺, ∅)‘suc 𝑏))
88	87	pweqd 4574	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (rec(𝐺, ∅)‘suc 𝑏) → 𝒫 dom 𝑥 = 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏))
89		imaeq1 6047	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (rec(𝐺, ∅)‘suc 𝑏) → (𝑥 “ 𝑦) = ((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦))
90	89	fveq2d 6887	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (rec(𝐺, ∅)‘suc 𝑏) → (𝐹‘(𝑥 “ 𝑦)) = (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)))
91	88, 90	mpteq12dv 5192	. . . . . . . . . . . . 13 ⊢ (𝑥 = (rec(𝐺, ∅)‘suc 𝑏) → (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦))))
92	59	dmex 7919	. . . . . . . . . . . . . . 15 ⊢ dom (rec(𝐺, ∅)‘suc 𝑏) ∈ V
93	92	pwex 5342	. . . . . . . . . . . . . 14 ⊢ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ∈ V
94	93	mptex 7227	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦))) ∈ V
95	91, 33, 94	fvmpt 6991	. . . . . . . . . . . 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 6884	. . . . . . . . . 10 ⊢ ((𝐺‘(rec(𝐺, ∅)‘suc 𝑏))‘𝑐) = ((𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)))‘𝑐)
98		r1tr 9776	. . . . . . . . . . . . . . 15 ⊢ Tr (𝑅1‘suc 𝑏)
99	98	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ ω → Tr (𝑅1‘suc 𝑏))
100		dftr4 5218	. . . . . . . . . . . . . 14 ⊢ (Tr (𝑅1‘suc 𝑏) ↔ (𝑅1‘suc 𝑏) ⊆ 𝒫 (𝑅1‘suc 𝑏))
101	99, 100	sylib 221	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ ω → (𝑅1‘suc 𝑏) ⊆ 𝒫 (𝑅1‘suc 𝑏))
102	101	sselda 3931	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝑐 ∈ 𝒫 (𝑅1‘suc 𝑏))
103		f1odm 6826	. . . . . . . . . . . . . . 15 ⊢ ((rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏)) → dom (rec(𝐺, ∅)‘suc 𝑏) = (𝑅1‘suc 𝑏))
104	35, 103	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ ω → dom (rec(𝐺, ∅)‘suc 𝑏) = (𝑅1‘suc 𝑏))
105	104	pweqd 4574	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ ω → 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) = 𝒫 (𝑅1‘suc 𝑏))
106	105	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) = 𝒫 (𝑅1‘suc 𝑏))
107	102, 106	eleqtrrd 2864	. . . . . . . . . . 11 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝑐 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏))
108		imaeq2 6048	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑐 → ((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦) = ((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐))
109	108	fveq2d 6887	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑐 → (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)) = (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐)))
110		eqid 2761	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦))) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)))
111		fvex 6896	. . . . . . . . . . . 12 ⊢ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐)) ∈ V
112	109, 110, 111	fvmpt 6991	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) → ((𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)))‘𝑐) = (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐)))
113	107, 112	syl 18	. . . . . . . . . 10 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)))‘𝑐) = (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐)))
114	97, 113	eqtrid 2808	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((𝐺‘(rec(𝐺, ∅)‘suc 𝑏))‘𝑐) = (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐)))
115	58, 86, 114	3eqtr4d 2806	. . . . . . . 8 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘suc 𝑏))‘𝑐))
116	115	adantlr 728	. . . . . . 7 ⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘suc 𝑏))‘𝑐))
117		fveq2 6883	. . . . . . . . 9 ⊢ ((rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → (𝐺‘(rec(𝐺, ∅)‘𝑏)) = (𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))))
118	117	fveq1d 6885	. . . . . . . 8 ⊢ ((rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → ((𝐺‘(rec(𝐺, ∅)‘𝑏))‘𝑐) = ((𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))‘𝑐))
119	118	ad2antlr 740	. . . . . . 7 ⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((𝐺‘(rec(𝐺, ∅)‘𝑏))‘𝑐) = ((𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))‘𝑐))
120		rdgsuc 8425	. . . . . . . . . 10 ⊢ (suc 𝑏 ∈ On → (rec(𝐺, ∅)‘suc suc 𝑏) = (𝐺‘(rec(𝐺, ∅)‘suc 𝑏)))
121	44, 120	syl 18	. . . . . . . . 9 ⊢ (𝑏 ∈ ω → (rec(𝐺, ∅)‘suc suc 𝑏) = (𝐺‘(rec(𝐺, ∅)‘suc 𝑏)))
122	121	fveq1d 6885	. . . . . . . 8 ⊢ (𝑏 ∈ ω → ((rec(𝐺, ∅)‘suc suc 𝑏)‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘suc 𝑏))‘𝑐))
123	122	ad2antrr 739	. . . . . . 7 ⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((rec(𝐺, ∅)‘suc suc 𝑏)‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘suc 𝑏))‘𝑐))
124	116, 119, 123	3eqtr4rd 2807	. . . . . 6 ⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((rec(𝐺, ∅)‘suc suc 𝑏)‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘𝑏))‘𝑐))
125		fvres 6902	. . . . . . 7 ⊢ (𝑐 ∈ (𝑅1‘suc 𝑏) → (((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏))‘𝑐) = ((rec(𝐺, ∅)‘suc suc 𝑏)‘𝑐))
126	125	adantl 487	. . . . . 6 ⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → (((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏))‘𝑐) = ((rec(𝐺, ∅)‘suc suc 𝑏)‘𝑐))
127		rdgsuc 8425	. . . . . . . . 9 ⊢ (𝑏 ∈ On → (rec(𝐺, ∅)‘suc 𝑏) = (𝐺‘(rec(𝐺, ∅)‘𝑏)))
128	50, 127	syl 18	. . . . . . . 8 ⊢ (𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏) = (𝐺‘(rec(𝐺, ∅)‘𝑏)))
129	128	fveq1d 6885	. . . . . . 7 ⊢ (𝑏 ∈ ω → ((rec(𝐺, ∅)‘suc 𝑏)‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘𝑏))‘𝑐))
130	129	ad2antrr 739	. . . . . 6 ⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((rec(𝐺, ∅)‘suc 𝑏)‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘𝑏))‘𝑐))
131	124, 126, 130	3eqtr4rd 2807	. . . . 5 ⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((rec(𝐺, ∅)‘suc 𝑏)‘𝑐) = (((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏))‘𝑐))
132	38, 49, 131	eqfnfvd 7030	. . . 4 ⊢ ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) → (rec(𝐺, ∅)‘suc 𝑏) = ((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏)))
133	132	ex 418	. . 3 ⊢ (𝑏 ∈ ω → ((rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → (rec(𝐺, ∅)‘suc 𝑏) = ((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏))))
134	6, 12, 18, 24, 30, 133	finds 7906	. 2 ⊢ (𝐴 ∈ ω → (rec(𝐺, ∅)‘𝐴) = ((rec(𝐺, ∅)‘suc 𝐴) ↾ (𝑅1‘𝐴)))
135		resss 5992	. 2 ⊢ ((rec(𝐺, ∅)‘suc 𝐴) ↾ (𝑅1‘𝐴)) ⊆ (rec(𝐺, ∅)‘suc 𝐴)
136	134, 135	eqsstrdi 3975	1 ⊢ (𝐴 ∈ ω → (rec(𝐺, ∅)‘𝐴) ⊆ (rec(𝐺, ∅)‘suc 𝐴))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  Vcvv 3451   ∩ cin 3898   ⊆ wss 3899  ∅c0 4279  𝒫 cpw 4557  {csn 4584  ∪ ciun 4951   ↦ cmpt 5186  Tr wtr 5212   × cxp 5649  dom cdm 5651   ↾ cres 5653   “ cima 5654  Oncon0 6361  suc csuc 6363   Fn wfn 6532  –1-1-onto→wf1o 6536  ‘cfv 6537  ωcom 7875  reccrdg 8410  Fincfn 8966  𝑅₁cr1 9759  cardccrd 10009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7421  df-oprab 7422  df-mpo 7423  df-om 7876  df-1st 7999  df-2nd 8000  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-1o 8469  df-2o 8470  df-oadd 8473  df-er 8710  df-map 8842  df-en 8967  df-dom 8968  df-sdom 8969  df-fin 8970  df-r1 9761  df-dju 9975  df-card 10013

This theorem is used by:  ackbij2lem4  10312