Theorem ackbij2lem3 10142

Description: Lemma for ackbij2 10144. (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 6831	. . . 4 ⊢ (𝑎 = ∅ → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘∅))
2		suceq 6382	. . . . . 6 ⊢ (𝑎 = ∅ → suc 𝑎 = suc ∅)
3	2	fveq2d 6835	. . . . 5 ⊢ (𝑎 = ∅ → (rec(𝐺, ∅)‘suc 𝑎) = (rec(𝐺, ∅)‘suc ∅))
4		fveq2 6831	. . . . 5 ⊢ (𝑎 = ∅ → (𝑅1‘𝑎) = (𝑅1‘∅))
5	3, 4	reseq12d 5936	. . . 4 ⊢ (𝑎 = ∅ → ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) = ((rec(𝐺, ∅)‘suc ∅) ↾ (𝑅1‘∅)))
6	1, 5	eqeq12d 2749	. . 3 ⊢ (𝑎 = ∅ → ((rec(𝐺, ∅)‘𝑎) = ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) ↔ (rec(𝐺, ∅)‘∅) = ((rec(𝐺, ∅)‘suc ∅) ↾ (𝑅1‘∅))))
7		fveq2 6831	. . . 4 ⊢ (𝑎 = 𝑏 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘𝑏))
8		suceq 6382	. . . . . 6 ⊢ (𝑎 = 𝑏 → suc 𝑎 = suc 𝑏)
9	8	fveq2d 6835	. . . . 5 ⊢ (𝑎 = 𝑏 → (rec(𝐺, ∅)‘suc 𝑎) = (rec(𝐺, ∅)‘suc 𝑏))
10		fveq2 6831	. . . . 5 ⊢ (𝑎 = 𝑏 → (𝑅1‘𝑎) = (𝑅1‘𝑏))
11	9, 10	reseq12d 5936	. . . 4 ⊢ (𝑎 = 𝑏 → ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))
12	7, 11	eqeq12d 2749	. . 3 ⊢ (𝑎 = 𝑏 → ((rec(𝐺, ∅)‘𝑎) = ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) ↔ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))))
13		fveq2 6831	. . . 4 ⊢ (𝑎 = suc 𝑏 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘suc 𝑏))
14		suceq 6382	. . . . . 6 ⊢ (𝑎 = suc 𝑏 → suc 𝑎 = suc suc 𝑏)
15	14	fveq2d 6835	. . . . 5 ⊢ (𝑎 = suc 𝑏 → (rec(𝐺, ∅)‘suc 𝑎) = (rec(𝐺, ∅)‘suc suc 𝑏))
16		fveq2 6831	. . . . 5 ⊢ (𝑎 = suc 𝑏 → (𝑅1‘𝑎) = (𝑅1‘suc 𝑏))
17	15, 16	reseq12d 5936	. . . 4 ⊢ (𝑎 = suc 𝑏 → ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) = ((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏)))
18	13, 17	eqeq12d 2749	. . 3 ⊢ (𝑎 = suc 𝑏 → ((rec(𝐺, ∅)‘𝑎) = ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) ↔ (rec(𝐺, ∅)‘suc 𝑏) = ((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏))))
19		fveq2 6831	. . . 4 ⊢ (𝑎 = 𝐴 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘𝐴))
20		suceq 6382	. . . . . 6 ⊢ (𝑎 = 𝐴 → suc 𝑎 = suc 𝐴)
21	20	fveq2d 6835	. . . . 5 ⊢ (𝑎 = 𝐴 → (rec(𝐺, ∅)‘suc 𝑎) = (rec(𝐺, ∅)‘suc 𝐴))
22		fveq2 6831	. . . . 5 ⊢ (𝑎 = 𝐴 → (𝑅1‘𝑎) = (𝑅1‘𝐴))
23	21, 22	reseq12d 5936	. . . 4 ⊢ (𝑎 = 𝐴 → ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) = ((rec(𝐺, ∅)‘suc 𝐴) ↾ (𝑅1‘𝐴)))
24	19, 23	eqeq12d 2749	. . 3 ⊢ (𝑎 = 𝐴 → ((rec(𝐺, ∅)‘𝑎) = ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) ↔ (rec(𝐺, ∅)‘𝐴) = ((rec(𝐺, ∅)‘suc 𝐴) ↾ (𝑅1‘𝐴))))
25		res0 5939	. . . 4 ⊢ ((rec(𝐺, ∅)‘suc ∅) ↾ ∅) = ∅
26		r10 9672	. . . . 5 ⊢ (𝑅1‘∅) = ∅
27	26	reseq2i 5932	. . . 4 ⊢ ((rec(𝐺, ∅)‘suc ∅) ↾ (𝑅1‘∅)) = ((rec(𝐺, ∅)‘suc ∅) ↾ ∅)
28		0ex 5249	. . . . 5 ⊢ ∅ ∈ V
29	28	rdg0 8349	. . . 4 ⊢ (rec(𝐺, ∅)‘∅) = ∅
30	25, 27, 29	3eqtr4ri 2767	. . 3 ⊢ (rec(𝐺, ∅)‘∅) = ((rec(𝐺, ∅)‘suc ∅) ↾ (𝑅1‘∅))
31		peano2 7829	. . . . . . . 8 ⊢ (𝑏 ∈ ω → suc 𝑏 ∈ ω)
32		ackbij.f	. . . . . . . . 9 ⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))
33		ackbij.g	. . . . . . . . 9 ⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))))
34	32, 33	ackbij2lem2 10141	. . . . . . . 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 6772	. . . . . . 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 480	. . . . 5 ⊢ ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) → (rec(𝐺, ∅)‘suc 𝑏) Fn (𝑅1‘suc 𝑏))
39		peano2 7829	. . . . . . . 8 ⊢ (suc 𝑏 ∈ ω → suc suc 𝑏 ∈ ω)
40	32, 33	ackbij2lem2 10141	. . . . . . . 8 ⊢ (suc suc 𝑏 ∈ ω → (rec(𝐺, ∅)‘suc suc 𝑏):(𝑅1‘suc suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc suc 𝑏)))
41		f1ofn 6772	. . . . . . . 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 7811	. . . . . . . . 9 ⊢ (suc 𝑏 ∈ ω → suc 𝑏 ∈ On)
44	31, 43	syl 17	. . . . . . . 8 ⊢ (𝑏 ∈ ω → suc 𝑏 ∈ On)
45		r1sssuc 9687	. . . . . . . 8 ⊢ (suc 𝑏 ∈ On → (𝑅1‘suc 𝑏) ⊆ (𝑅1‘suc suc 𝑏))
46	44, 45	syl 17	. . . . . . 7 ⊢ (𝑏 ∈ ω → (𝑅1‘suc 𝑏) ⊆ (𝑅1‘suc suc 𝑏))
47		fnssres 6612	. . . . . . 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 480	. . . . 5 ⊢ ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) → ((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏)) Fn (𝑅1‘suc 𝑏))
50		nnon 7811	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ ω → 𝑏 ∈ On)
51		r1suc 9674	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ On → (𝑅1‘suc 𝑏) = 𝒫 (𝑅1‘𝑏))
52	50, 51	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ ω → (𝑅1‘suc 𝑏) = 𝒫 (𝑅1‘𝑏))
53	52	eleq2d 2819	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ ω → (𝑐 ∈ (𝑅1‘suc 𝑏) ↔ 𝑐 ∈ 𝒫 (𝑅1‘𝑏)))
54	53	biimpa 476	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝑐 ∈ 𝒫 (𝑅1‘𝑏))
55	54	elpwid 4560	. . . . . . . . . . 11 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝑐 ⊆ (𝑅1‘𝑏))
56		resima2 5972	. . . . . . . . . . 11 ⊢ (𝑐 ⊆ (𝑅1‘𝑏) → (((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐) = ((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐))
57	55, 56	syl 17	. . . . . . . . . 10 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → (((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐) = ((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐))
58	57	fveq2d 6835	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐)) = (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐)))
59		fvex 6844	. . . . . . . . . . . . 13 ⊢ (rec(𝐺, ∅)‘suc 𝑏) ∈ V
60	59	resex 5985	. . . . . . . . . . . 12 ⊢ ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ∈ V
61		dmeq 5849	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → dom 𝑥 = dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))
62	61	pweqd 4568	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → 𝒫 dom 𝑥 = 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))
63		imaeq1 6011	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → (𝑥 “ 𝑦) = (((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦))
64	63	fveq2d 6835	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → (𝐹‘(𝑥 “ 𝑦)) = (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)))
65	62, 64	mpteq12dv 5182	. . . . . . . . . . . . 13 ⊢ (𝑥 = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))) = (𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦))))
66	60	dmex 7848	. . . . . . . . . . . . . . 15 ⊢ dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ∈ V
67	66	pwex 5322	. . . . . . . . . . . . . 14 ⊢ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ∈ V
68	67	mptex 7166	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦))) ∈ V
69	65, 33, 68	fvmpt 6938	. . . . . . . . . . . 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 6832	. . . . . . . . . 10 ⊢ ((𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))‘𝑐) = ((𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)))‘𝑐)
72		r1sssuc 9687	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ On → (𝑅1‘𝑏) ⊆ (𝑅1‘suc 𝑏))
73	50, 72	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ ω → (𝑅1‘𝑏) ⊆ (𝑅1‘suc 𝑏))
74		fnssres 6612	. . . . . . . . . . . . . . . 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 6594	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ ω → dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) = (𝑅1‘𝑏))
77	76	pweqd 4568	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ ω → 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) = 𝒫 (𝑅1‘𝑏))
78	77	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) = 𝒫 (𝑅1‘𝑏))
79	54, 78	eleqtrrd 2836	. . . . . . . . . . 11 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝑐 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))
80		imaeq2 6012	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑐 → (((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦) = (((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐))
81	80	fveq2d 6835	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑐 → (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)) = (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐)))
82		eqid 2733	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦))) = (𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)))
83		fvex 6844	. . . . . . . . . . . 12 ⊢ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐)) ∈ V
84	81, 82, 83	fvmpt 6938	. . . . . . . . . . 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 2780	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))‘𝑐) = (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐)))
87		dmeq 5849	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (rec(𝐺, ∅)‘suc 𝑏) → dom 𝑥 = dom (rec(𝐺, ∅)‘suc 𝑏))
88	87	pweqd 4568	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (rec(𝐺, ∅)‘suc 𝑏) → 𝒫 dom 𝑥 = 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏))
89		imaeq1 6011	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (rec(𝐺, ∅)‘suc 𝑏) → (𝑥 “ 𝑦) = ((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦))
90	89	fveq2d 6835	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (rec(𝐺, ∅)‘suc 𝑏) → (𝐹‘(𝑥 “ 𝑦)) = (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)))
91	88, 90	mpteq12dv 5182	. . . . . . . . . . . . 13 ⊢ (𝑥 = (rec(𝐺, ∅)‘suc 𝑏) → (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦))))
92	59	dmex 7848	. . . . . . . . . . . . . . 15 ⊢ dom (rec(𝐺, ∅)‘suc 𝑏) ∈ V
93	92	pwex 5322	. . . . . . . . . . . . . 14 ⊢ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ∈ V
94	93	mptex 7166	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦))) ∈ V
95	91, 33, 94	fvmpt 6938	. . . . . . . . . . . 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 6832	. . . . . . . . . 10 ⊢ ((𝐺‘(rec(𝐺, ∅)‘suc 𝑏))‘𝑐) = ((𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)))‘𝑐)
98		r1tr 9680	. . . . . . . . . . . . . . 15 ⊢ Tr (𝑅1‘suc 𝑏)
99	98	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ ω → Tr (𝑅1‘suc 𝑏))
100		dftr4 5208	. . . . . . . . . . . . . 14 ⊢ (Tr (𝑅1‘suc 𝑏) ↔ (𝑅1‘suc 𝑏) ⊆ 𝒫 (𝑅1‘suc 𝑏))
101	99, 100	sylib 218	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ ω → (𝑅1‘suc 𝑏) ⊆ 𝒫 (𝑅1‘suc 𝑏))
102	101	sselda 3930	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝑐 ∈ 𝒫 (𝑅1‘suc 𝑏))
103		f1odm 6775	. . . . . . . . . . . . . . 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 4568	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ ω → 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) = 𝒫 (𝑅1‘suc 𝑏))
106	105	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) = 𝒫 (𝑅1‘suc 𝑏))
107	102, 106	eleqtrrd 2836	. . . . . . . . . . 11 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝑐 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏))
108		imaeq2 6012	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑐 → ((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦) = ((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐))
109	108	fveq2d 6835	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑐 → (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)) = (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐)))
110		eqid 2733	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦))) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)))
111		fvex 6844	. . . . . . . . . . . 12 ⊢ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐)) ∈ V
112	109, 110, 111	fvmpt 6938	. . . . . . . . . . 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 2780	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((𝐺‘(rec(𝐺, ∅)‘suc 𝑏))‘𝑐) = (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐)))
115	58, 86, 114	3eqtr4d 2778	. . . . . . . 8 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘suc 𝑏))‘𝑐))
116	115	adantlr 715	. . . . . . 7 ⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘suc 𝑏))‘𝑐))
117		fveq2 6831	. . . . . . . . 9 ⊢ ((rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → (𝐺‘(rec(𝐺, ∅)‘𝑏)) = (𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))))
118	117	fveq1d 6833	. . . . . . . 8 ⊢ ((rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → ((𝐺‘(rec(𝐺, ∅)‘𝑏))‘𝑐) = ((𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))‘𝑐))
119	118	ad2antlr 727	. . . . . . 7 ⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((𝐺‘(rec(𝐺, ∅)‘𝑏))‘𝑐) = ((𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))‘𝑐))
120		rdgsuc 8352	. . . . . . . . . 10 ⊢ (suc 𝑏 ∈ On → (rec(𝐺, ∅)‘suc suc 𝑏) = (𝐺‘(rec(𝐺, ∅)‘suc 𝑏)))
121	44, 120	syl 17	. . . . . . . . 9 ⊢ (𝑏 ∈ ω → (rec(𝐺, ∅)‘suc suc 𝑏) = (𝐺‘(rec(𝐺, ∅)‘suc 𝑏)))
122	121	fveq1d 6833	. . . . . . . 8 ⊢ (𝑏 ∈ ω → ((rec(𝐺, ∅)‘suc suc 𝑏)‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘suc 𝑏))‘𝑐))
123	122	ad2antrr 726	. . . . . . 7 ⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((rec(𝐺, ∅)‘suc suc 𝑏)‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘suc 𝑏))‘𝑐))
124	116, 119, 123	3eqtr4rd 2779	. . . . . 6 ⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((rec(𝐺, ∅)‘suc suc 𝑏)‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘𝑏))‘𝑐))
125		fvres 6850	. . . . . . 7 ⊢ (𝑐 ∈ (𝑅1‘suc 𝑏) → (((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏))‘𝑐) = ((rec(𝐺, ∅)‘suc suc 𝑏)‘𝑐))
126	125	adantl 481	. . . . . 6 ⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → (((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏))‘𝑐) = ((rec(𝐺, ∅)‘suc suc 𝑏)‘𝑐))
127		rdgsuc 8352	. . . . . . . . 9 ⊢ (𝑏 ∈ On → (rec(𝐺, ∅)‘suc 𝑏) = (𝐺‘(rec(𝐺, ∅)‘𝑏)))
128	50, 127	syl 17	. . . . . . . 8 ⊢ (𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏) = (𝐺‘(rec(𝐺, ∅)‘𝑏)))
129	128	fveq1d 6833	. . . . . . 7 ⊢ (𝑏 ∈ ω → ((rec(𝐺, ∅)‘suc 𝑏)‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘𝑏))‘𝑐))
130	129	ad2antrr 726	. . . . . 6 ⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((rec(𝐺, ∅)‘suc 𝑏)‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘𝑏))‘𝑐))
131	124, 126, 130	3eqtr4rd 2779	. . . . 5 ⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((rec(𝐺, ∅)‘suc 𝑏)‘𝑐) = (((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏))‘𝑐))
132	38, 49, 131	eqfnfvd 6976	. . . 4 ⊢ ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) → (rec(𝐺, ∅)‘suc 𝑏) = ((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏)))
133	132	ex 412	. . 3 ⊢ (𝑏 ∈ ω → ((rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → (rec(𝐺, ∅)‘suc 𝑏) = ((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏))))
134	6, 12, 18, 24, 30, 133	finds 7835	. 2 ⊢ (𝐴 ∈ ω → (rec(𝐺, ∅)‘𝐴) = ((rec(𝐺, ∅)‘suc 𝐴) ↾ (𝑅1‘𝐴)))
135		resss 5957	. 2 ⊢ ((rec(𝐺, ∅)‘suc 𝐴) ↾ (𝑅1‘𝐴)) ⊆ (rec(𝐺, ∅)‘suc 𝐴)
136	134, 135	eqsstrdi 3975	1 ⊢ (𝐴 ∈ ω → (rec(𝐺, ∅)‘𝐴) ⊆ (rec(𝐺, ∅)‘suc 𝐴))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  Vcvv 3437   ∩ cin 3897   ⊆ wss 3898  ∅c0 4282  𝒫 cpw 4551  {csn 4577  ∪ ciun 4943   ↦ cmpt 5176  Tr wtr 5202   × cxp 5619  dom cdm 5621   ↾ cres 5623   “ cima 5624  Oncon0 6314  suc csuc 6316   Fn wfn 6484  –1-1-onto→wf1o 6488  ‘cfv 6489  ωcom 7805  reccrdg 8337  Fincfn 8879  𝑅₁cr1 9666  cardccrd 9839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-rep 5221  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-int 4900  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-ov 7358  df-oprab 7359  df-mpo 7360  df-om 7806  df-1st 7930  df-2nd 7931  df-frecs 8220  df-wrecs 8251  df-recs 8300  df-rdg 8338  df-1o 8394  df-2o 8395  df-oadd 8398  df-er 8631  df-map 8761  df-en 8880  df-dom 8881  df-sdom 8882  df-fin 8883  df-r1 9668  df-dju 9805  df-card 9843

This theorem is referenced by:  ackbij2lem4  10143