Theorem ackbij2lem3 10200

Description: Lemma for ackbij2 10202. (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 6861	. . . 4 ⊢ (𝑎 = ∅ → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘∅))
2		suceq 6403	. . . . . 6 ⊢ (𝑎 = ∅ → suc 𝑎 = suc ∅)
3	2	fveq2d 6865	. . . . 5 ⊢ (𝑎 = ∅ → (rec(𝐺, ∅)‘suc 𝑎) = (rec(𝐺, ∅)‘suc ∅))
4		fveq2 6861	. . . . 5 ⊢ (𝑎 = ∅ → (𝑅1‘𝑎) = (𝑅1‘∅))
5	3, 4	reseq12d 5954	. . . 4 ⊢ (𝑎 = ∅ → ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) = ((rec(𝐺, ∅)‘suc ∅) ↾ (𝑅1‘∅)))
6	1, 5	eqeq12d 2746	. . 3 ⊢ (𝑎 = ∅ → ((rec(𝐺, ∅)‘𝑎) = ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) ↔ (rec(𝐺, ∅)‘∅) = ((rec(𝐺, ∅)‘suc ∅) ↾ (𝑅1‘∅))))
7		fveq2 6861	. . . 4 ⊢ (𝑎 = 𝑏 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘𝑏))
8		suceq 6403	. . . . . 6 ⊢ (𝑎 = 𝑏 → suc 𝑎 = suc 𝑏)
9	8	fveq2d 6865	. . . . 5 ⊢ (𝑎 = 𝑏 → (rec(𝐺, ∅)‘suc 𝑎) = (rec(𝐺, ∅)‘suc 𝑏))
10		fveq2 6861	. . . . 5 ⊢ (𝑎 = 𝑏 → (𝑅1‘𝑎) = (𝑅1‘𝑏))
11	9, 10	reseq12d 5954	. . . 4 ⊢ (𝑎 = 𝑏 → ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))
12	7, 11	eqeq12d 2746	. . 3 ⊢ (𝑎 = 𝑏 → ((rec(𝐺, ∅)‘𝑎) = ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) ↔ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))))
13		fveq2 6861	. . . 4 ⊢ (𝑎 = suc 𝑏 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘suc 𝑏))
14		suceq 6403	. . . . . 6 ⊢ (𝑎 = suc 𝑏 → suc 𝑎 = suc suc 𝑏)
15	14	fveq2d 6865	. . . . 5 ⊢ (𝑎 = suc 𝑏 → (rec(𝐺, ∅)‘suc 𝑎) = (rec(𝐺, ∅)‘suc suc 𝑏))
16		fveq2 6861	. . . . 5 ⊢ (𝑎 = suc 𝑏 → (𝑅1‘𝑎) = (𝑅1‘suc 𝑏))
17	15, 16	reseq12d 5954	. . . 4 ⊢ (𝑎 = suc 𝑏 → ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) = ((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏)))
18	13, 17	eqeq12d 2746	. . 3 ⊢ (𝑎 = suc 𝑏 → ((rec(𝐺, ∅)‘𝑎) = ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) ↔ (rec(𝐺, ∅)‘suc 𝑏) = ((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏))))
19		fveq2 6861	. . . 4 ⊢ (𝑎 = 𝐴 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘𝐴))
20		suceq 6403	. . . . . 6 ⊢ (𝑎 = 𝐴 → suc 𝑎 = suc 𝐴)
21	20	fveq2d 6865	. . . . 5 ⊢ (𝑎 = 𝐴 → (rec(𝐺, ∅)‘suc 𝑎) = (rec(𝐺, ∅)‘suc 𝐴))
22		fveq2 6861	. . . . 5 ⊢ (𝑎 = 𝐴 → (𝑅1‘𝑎) = (𝑅1‘𝐴))
23	21, 22	reseq12d 5954	. . . 4 ⊢ (𝑎 = 𝐴 → ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) = ((rec(𝐺, ∅)‘suc 𝐴) ↾ (𝑅1‘𝐴)))
24	19, 23	eqeq12d 2746	. . 3 ⊢ (𝑎 = 𝐴 → ((rec(𝐺, ∅)‘𝑎) = ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) ↔ (rec(𝐺, ∅)‘𝐴) = ((rec(𝐺, ∅)‘suc 𝐴) ↾ (𝑅1‘𝐴))))
25		res0 5957	. . . 4 ⊢ ((rec(𝐺, ∅)‘suc ∅) ↾ ∅) = ∅
26		r10 9728	. . . . 5 ⊢ (𝑅1‘∅) = ∅
27	26	reseq2i 5950	. . . 4 ⊢ ((rec(𝐺, ∅)‘suc ∅) ↾ (𝑅1‘∅)) = ((rec(𝐺, ∅)‘suc ∅) ↾ ∅)
28		0ex 5265	. . . . 5 ⊢ ∅ ∈ V
29	28	rdg0 8392	. . . 4 ⊢ (rec(𝐺, ∅)‘∅) = ∅
30	25, 27, 29	3eqtr4ri 2764	. . 3 ⊢ (rec(𝐺, ∅)‘∅) = ((rec(𝐺, ∅)‘suc ∅) ↾ (𝑅1‘∅))
31		peano2 7869	. . . . . . . 8 ⊢ (𝑏 ∈ ω → suc 𝑏 ∈ ω)
32		ackbij.f	. . . . . . . . 9 ⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))
33		ackbij.g	. . . . . . . . 9 ⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))))
34	32, 33	ackbij2lem2 10199	. . . . . . . 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 6804	. . . . . . 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 7869	. . . . . . . 8 ⊢ (suc 𝑏 ∈ ω → suc suc 𝑏 ∈ ω)
40	32, 33	ackbij2lem2 10199	. . . . . . . 8 ⊢ (suc suc 𝑏 ∈ ω → (rec(𝐺, ∅)‘suc suc 𝑏):(𝑅1‘suc suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc suc 𝑏)))
41		f1ofn 6804	. . . . . . . 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 7851	. . . . . . . . 9 ⊢ (suc 𝑏 ∈ ω → suc 𝑏 ∈ On)
44	31, 43	syl 17	. . . . . . . 8 ⊢ (𝑏 ∈ ω → suc 𝑏 ∈ On)
45		r1sssuc 9743	. . . . . . . 8 ⊢ (suc 𝑏 ∈ On → (𝑅1‘suc 𝑏) ⊆ (𝑅1‘suc suc 𝑏))
46	44, 45	syl 17	. . . . . . 7 ⊢ (𝑏 ∈ ω → (𝑅1‘suc 𝑏) ⊆ (𝑅1‘suc suc 𝑏))
47		fnssres 6644	. . . . . . 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 7851	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ ω → 𝑏 ∈ On)
51		r1suc 9730	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ On → (𝑅1‘suc 𝑏) = 𝒫 (𝑅1‘𝑏))
52	50, 51	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ ω → (𝑅1‘suc 𝑏) = 𝒫 (𝑅1‘𝑏))
53	52	eleq2d 2815	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ ω → (𝑐 ∈ (𝑅1‘suc 𝑏) ↔ 𝑐 ∈ 𝒫 (𝑅1‘𝑏)))
54	53	biimpa 476	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝑐 ∈ 𝒫 (𝑅1‘𝑏))
55	54	elpwid 4575	. . . . . . . . . . 11 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝑐 ⊆ (𝑅1‘𝑏))
56		resima2 5990	. . . . . . . . . . 11 ⊢ (𝑐 ⊆ (𝑅1‘𝑏) → (((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐) = ((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐))
57	55, 56	syl 17	. . . . . . . . . 10 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → (((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐) = ((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐))
58	57	fveq2d 6865	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐)) = (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐)))
59		fvex 6874	. . . . . . . . . . . . 13 ⊢ (rec(𝐺, ∅)‘suc 𝑏) ∈ V
60	59	resex 6003	. . . . . . . . . . . 12 ⊢ ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ∈ V
61		dmeq 5870	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → dom 𝑥 = dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))
62	61	pweqd 4583	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → 𝒫 dom 𝑥 = 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))
63		imaeq1 6029	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → (𝑥 “ 𝑦) = (((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦))
64	63	fveq2d 6865	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → (𝐹‘(𝑥 “ 𝑦)) = (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)))
65	62, 64	mpteq12dv 5197	. . . . . . . . . . . . 13 ⊢ (𝑥 = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))) = (𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦))))
66	60	dmex 7888	. . . . . . . . . . . . . . 15 ⊢ dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ∈ V
67	66	pwex 5338	. . . . . . . . . . . . . 14 ⊢ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ∈ V
68	67	mptex 7200	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦))) ∈ V
69	65, 33, 68	fvmpt 6971	. . . . . . . . . . . 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 6862	. . . . . . . . . 10 ⊢ ((𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))‘𝑐) = ((𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)))‘𝑐)
72		r1sssuc 9743	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ On → (𝑅1‘𝑏) ⊆ (𝑅1‘suc 𝑏))
73	50, 72	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ ω → (𝑅1‘𝑏) ⊆ (𝑅1‘suc 𝑏))
74		fnssres 6644	. . . . . . . . . . . . . . . 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 6626	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ ω → dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) = (𝑅1‘𝑏))
77	76	pweqd 4583	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ ω → 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) = 𝒫 (𝑅1‘𝑏))
78	77	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) = 𝒫 (𝑅1‘𝑏))
79	54, 78	eleqtrrd 2832	. . . . . . . . . . 11 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝑐 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))
80		imaeq2 6030	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑐 → (((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦) = (((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐))
81	80	fveq2d 6865	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑐 → (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)) = (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐)))
82		eqid 2730	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦))) = (𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)))
83		fvex 6874	. . . . . . . . . . . 12 ⊢ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐)) ∈ V
84	81, 82, 83	fvmpt 6971	. . . . . . . . . . 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 2777	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))‘𝑐) = (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐)))
87		dmeq 5870	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (rec(𝐺, ∅)‘suc 𝑏) → dom 𝑥 = dom (rec(𝐺, ∅)‘suc 𝑏))
88	87	pweqd 4583	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (rec(𝐺, ∅)‘suc 𝑏) → 𝒫 dom 𝑥 = 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏))
89		imaeq1 6029	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (rec(𝐺, ∅)‘suc 𝑏) → (𝑥 “ 𝑦) = ((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦))
90	89	fveq2d 6865	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (rec(𝐺, ∅)‘suc 𝑏) → (𝐹‘(𝑥 “ 𝑦)) = (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)))
91	88, 90	mpteq12dv 5197	. . . . . . . . . . . . 13 ⊢ (𝑥 = (rec(𝐺, ∅)‘suc 𝑏) → (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦))))
92	59	dmex 7888	. . . . . . . . . . . . . . 15 ⊢ dom (rec(𝐺, ∅)‘suc 𝑏) ∈ V
93	92	pwex 5338	. . . . . . . . . . . . . 14 ⊢ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ∈ V
94	93	mptex 7200	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦))) ∈ V
95	91, 33, 94	fvmpt 6971	. . . . . . . . . . . 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 6862	. . . . . . . . . 10 ⊢ ((𝐺‘(rec(𝐺, ∅)‘suc 𝑏))‘𝑐) = ((𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)))‘𝑐)
98		r1tr 9736	. . . . . . . . . . . . . . 15 ⊢ Tr (𝑅1‘suc 𝑏)
99	98	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ ω → Tr (𝑅1‘suc 𝑏))
100		dftr4 5224	. . . . . . . . . . . . . 14 ⊢ (Tr (𝑅1‘suc 𝑏) ↔ (𝑅1‘suc 𝑏) ⊆ 𝒫 (𝑅1‘suc 𝑏))
101	99, 100	sylib 218	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ ω → (𝑅1‘suc 𝑏) ⊆ 𝒫 (𝑅1‘suc 𝑏))
102	101	sselda 3949	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝑐 ∈ 𝒫 (𝑅1‘suc 𝑏))
103		f1odm 6807	. . . . . . . . . . . . . . 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 4583	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ ω → 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) = 𝒫 (𝑅1‘suc 𝑏))
106	105	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) = 𝒫 (𝑅1‘suc 𝑏))
107	102, 106	eleqtrrd 2832	. . . . . . . . . . 11 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝑐 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏))
108		imaeq2 6030	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑐 → ((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦) = ((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐))
109	108	fveq2d 6865	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑐 → (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)) = (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐)))
110		eqid 2730	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦))) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)))
111		fvex 6874	. . . . . . . . . . . 12 ⊢ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐)) ∈ V
112	109, 110, 111	fvmpt 6971	. . . . . . . . . . 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 2777	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((𝐺‘(rec(𝐺, ∅)‘suc 𝑏))‘𝑐) = (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐)))
115	58, 86, 114	3eqtr4d 2775	. . . . . . . 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 6861	. . . . . . . . 9 ⊢ ((rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → (𝐺‘(rec(𝐺, ∅)‘𝑏)) = (𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))))
118	117	fveq1d 6863	. . . . . . . 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 8395	. . . . . . . . . 10 ⊢ (suc 𝑏 ∈ On → (rec(𝐺, ∅)‘suc suc 𝑏) = (𝐺‘(rec(𝐺, ∅)‘suc 𝑏)))
121	44, 120	syl 17	. . . . . . . . 9 ⊢ (𝑏 ∈ ω → (rec(𝐺, ∅)‘suc suc 𝑏) = (𝐺‘(rec(𝐺, ∅)‘suc 𝑏)))
122	121	fveq1d 6863	. . . . . . . 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 2776	. . . . . 6 ⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((rec(𝐺, ∅)‘suc suc 𝑏)‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘𝑏))‘𝑐))
125		fvres 6880	. . . . . . 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 8395	. . . . . . . . 9 ⊢ (𝑏 ∈ On → (rec(𝐺, ∅)‘suc 𝑏) = (𝐺‘(rec(𝐺, ∅)‘𝑏)))
128	50, 127	syl 17	. . . . . . . 8 ⊢ (𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏) = (𝐺‘(rec(𝐺, ∅)‘𝑏)))
129	128	fveq1d 6863	. . . . . . 7 ⊢ (𝑏 ∈ ω → ((rec(𝐺, ∅)‘suc 𝑏)‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘𝑏))‘𝑐))
130	129	ad2antrr 726	. . . . . 6 ⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((rec(𝐺, ∅)‘suc 𝑏)‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘𝑏))‘𝑐))
131	124, 126, 130	3eqtr4rd 2776	. . . . 5 ⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((rec(𝐺, ∅)‘suc 𝑏)‘𝑐) = (((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏))‘𝑐))
132	38, 49, 131	eqfnfvd 7009	. . . 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 7875	. 2 ⊢ (𝐴 ∈ ω → (rec(𝐺, ∅)‘𝐴) = ((rec(𝐺, ∅)‘suc 𝐴) ↾ (𝑅1‘𝐴)))
135		resss 5975	. 2 ⊢ ((rec(𝐺, ∅)‘suc 𝐴) ↾ (𝑅1‘𝐴)) ⊆ (rec(𝐺, ∅)‘suc 𝐴)
136	134, 135	eqsstrdi 3994	1 ⊢ (𝐴 ∈ ω → (rec(𝐺, ∅)‘𝐴) ⊆ (rec(𝐺, ∅)‘suc 𝐴))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3450   ∩ cin 3916   ⊆ wss 3917  ∅c0 4299  𝒫 cpw 4566  {csn 4592  ∪ ciun 4958   ↦ cmpt 5191  Tr wtr 5217   × cxp 5639  dom cdm 5641   ↾ cres 5643   “ cima 5644  Oncon0 6335  suc csuc 6337   Fn wfn 6509  –1-1-onto→wf1o 6513  ‘cfv 6514  ωcom 7845  reccrdg 8380  Fincfn 8921  𝑅₁cr1 9722  cardccrd 9895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-int 4914  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395  df-om 7846  df-1st 7971  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-1o 8437  df-2o 8438  df-oadd 8441  df-er 8674  df-map 8804  df-en 8922  df-dom 8923  df-sdom 8924  df-fin 8925  df-r1 9724  df-dju 9861  df-card 9899

This theorem is referenced by:  ackbij2lem4  10201