Theorem ackbij2lem3 10357

Description: Lemma for ackbij2 10359. (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 6916	. . . 4 ⊢ (𝑎 = ∅ → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘∅))
2		suceq 6457	. . . . . 6 ⊢ (𝑎 = ∅ → suc 𝑎 = suc ∅)
3	2	fveq2d 6920	. . . . 5 ⊢ (𝑎 = ∅ → (rec(𝐺, ∅)‘suc 𝑎) = (rec(𝐺, ∅)‘suc ∅))
4		fveq2 6916	. . . . 5 ⊢ (𝑎 = ∅ → (𝑅1‘𝑎) = (𝑅1‘∅))
5	3, 4	reseq12d 5987	. . . 4 ⊢ (𝑎 = ∅ → ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) = ((rec(𝐺, ∅)‘suc ∅) ↾ (𝑅1‘∅)))
6	1, 5	eqeq12d 2779	. . 3 ⊢ (𝑎 = ∅ → ((rec(𝐺, ∅)‘𝑎) = ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) ↔ (rec(𝐺, ∅)‘∅) = ((rec(𝐺, ∅)‘suc ∅) ↾ (𝑅1‘∅))))
7		fveq2 6916	. . . 4 ⊢ (𝑎 = 𝑏 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘𝑏))
8		suceq 6457	. . . . . 6 ⊢ (𝑎 = 𝑏 → suc 𝑎 = suc 𝑏)
9	8	fveq2d 6920	. . . . 5 ⊢ (𝑎 = 𝑏 → (rec(𝐺, ∅)‘suc 𝑎) = (rec(𝐺, ∅)‘suc 𝑏))
10		fveq2 6916	. . . . 5 ⊢ (𝑎 = 𝑏 → (𝑅1‘𝑎) = (𝑅1‘𝑏))
11	9, 10	reseq12d 5987	. . . 4 ⊢ (𝑎 = 𝑏 → ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))
12	7, 11	eqeq12d 2779	. . 3 ⊢ (𝑎 = 𝑏 → ((rec(𝐺, ∅)‘𝑎) = ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) ↔ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))))
13		fveq2 6916	. . . 4 ⊢ (𝑎 = suc 𝑏 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘suc 𝑏))
14		suceq 6457	. . . . . 6 ⊢ (𝑎 = suc 𝑏 → suc 𝑎 = suc suc 𝑏)
15	14	fveq2d 6920	. . . . 5 ⊢ (𝑎 = suc 𝑏 → (rec(𝐺, ∅)‘suc 𝑎) = (rec(𝐺, ∅)‘suc suc 𝑏))
16		fveq2 6916	. . . . 5 ⊢ (𝑎 = suc 𝑏 → (𝑅1‘𝑎) = (𝑅1‘suc 𝑏))
17	15, 16	reseq12d 5987	. . . 4 ⊢ (𝑎 = suc 𝑏 → ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) = ((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏)))
18	13, 17	eqeq12d 2779	. . 3 ⊢ (𝑎 = suc 𝑏 → ((rec(𝐺, ∅)‘𝑎) = ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) ↔ (rec(𝐺, ∅)‘suc 𝑏) = ((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏))))
19		fveq2 6916	. . . 4 ⊢ (𝑎 = 𝐴 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘𝐴))
20		suceq 6457	. . . . . 6 ⊢ (𝑎 = 𝐴 → suc 𝑎 = suc 𝐴)
21	20	fveq2d 6920	. . . . 5 ⊢ (𝑎 = 𝐴 → (rec(𝐺, ∅)‘suc 𝑎) = (rec(𝐺, ∅)‘suc 𝐴))
22		fveq2 6916	. . . . 5 ⊢ (𝑎 = 𝐴 → (𝑅1‘𝑎) = (𝑅1‘𝐴))
23	21, 22	reseq12d 5987	. . . 4 ⊢ (𝑎 = 𝐴 → ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) = ((rec(𝐺, ∅)‘suc 𝐴) ↾ (𝑅1‘𝐴)))
24	19, 23	eqeq12d 2779	. . 3 ⊢ (𝑎 = 𝐴 → ((rec(𝐺, ∅)‘𝑎) = ((rec(𝐺, ∅)‘suc 𝑎) ↾ (𝑅1‘𝑎)) ↔ (rec(𝐺, ∅)‘𝐴) = ((rec(𝐺, ∅)‘suc 𝐴) ↾ (𝑅1‘𝐴))))
25		res0 5990	. . . 4 ⊢ ((rec(𝐺, ∅)‘suc ∅) ↾ ∅) = ∅
26		r10 9812	. . . . 5 ⊢ (𝑅1‘∅) = ∅
27	26	reseq2i 5983	. . . 4 ⊢ ((rec(𝐺, ∅)‘suc ∅) ↾ (𝑅1‘∅)) = ((rec(𝐺, ∅)‘suc ∅) ↾ ∅)
28		0ex 5267	. . . . 5 ⊢ ∅ ∈ V
29	28	rdg0 8467	. . . 4 ⊢ (rec(𝐺, ∅)‘∅) = ∅
30	25, 27, 29	3eqtr4ri 2797	. . 3 ⊢ (rec(𝐺, ∅)‘∅) = ((rec(𝐺, ∅)‘suc ∅) ↾ (𝑅1‘∅))
31		peano2 7935	. . . . . . . 8 ⊢ (𝑏 ∈ ω → suc 𝑏 ∈ ω)
32		ackbij.f	. . . . . . . . 9 ⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))
33		ackbij.g	. . . . . . . . 9 ⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))))
34	32, 33	ackbij2lem2 10356	. . . . . . . 8 ⊢ (suc 𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)⟶1-1onto(card‘(𝑅1‘suc 𝑏)))
35	31, 34	syl 18	. . . . . . 7 ⊢ (𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)⟶1-1onto(card‘(𝑅1‘suc 𝑏)))
36		f1ofn 6855	. . . . . . 7 ⊢ ((rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)⟶1-1onto(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 7935	. . . . . . . 8 ⊢ (suc 𝑏 ∈ ω → suc suc 𝑏 ∈ ω)
40	32, 33	ackbij2lem2 10356	. . . . . . . 8 ⊢ (suc suc 𝑏 ∈ ω → (rec(𝐺, ∅)‘suc suc 𝑏):(𝑅1‘suc suc 𝑏)⟶1-1onto(card‘(𝑅1‘suc suc 𝑏)))
41		f1ofn 6855	. . . . . . . 8 ⊢ ((rec(𝐺, ∅)‘suc suc 𝑏):(𝑅1‘suc suc 𝑏)⟶1-1onto(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 7917	. . . . . . . . 9 ⊢ (suc 𝑏 ∈ ω → suc 𝑏 ∈ On)
44	31, 43	syl 18	. . . . . . . 8 ⊢ (𝑏 ∈ ω → suc 𝑏 ∈ On)
45		r1sssuc 9827	. . . . . . . 8 ⊢ (suc 𝑏 ∈ On → (𝑅1‘suc 𝑏) ⊆ (𝑅1‘suc suc 𝑏))
46	44, 45	syl 18	. . . . . . 7 ⊢ (𝑏 ∈ ω → (𝑅1‘suc 𝑏) ⊆ (𝑅1‘suc suc 𝑏))
47		fnssres 6692	. . . . . . 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 7917	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ ω → 𝑏 ∈ On)
51		r1suc 9814	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ On → (𝑅1‘suc 𝑏) = 𝒫 (𝑅1‘𝑏))
52	50, 51	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ ω → (𝑅1‘suc 𝑏) = 𝒫 (𝑅1‘𝑏))
53	52	eleq2d 2850	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ ω → (𝑐 ∈ (𝑅1‘suc 𝑏) ↔ 𝑐 ∈ 𝒫 (𝑅1‘𝑏)))
54	53	biimpa 482	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝑐 ∈ 𝒫 (𝑅1‘𝑏))
55	54	elpwid 4569	. . . . . . . . . . 11 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝑐 ⊆ (𝑅1‘𝑏))
56		resima2 6075	. . . . . . . . . . 11 ⊢ (𝑐 ⊆ (𝑅1‘𝑏) → (((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐) = ((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐))
57	55, 56	syl 18	. . . . . . . . . 10 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → (((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐) = ((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐))
58	57	fveq2d 6920	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐)) = (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐)))
59		fvex 6929	. . . . . . . . . . . . 13 ⊢ (rec(𝐺, ∅)‘suc 𝑏) ∈ V
60	59	resex 6036	. . . . . . . . . . . 12 ⊢ ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ∈ V
61		dmeq 5897	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → dom 𝑥 = dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))
62	61	pweqd 4577	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → 𝒫 dom 𝑥 = 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))
63		imaeq1 6065	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → (𝑥 “ 𝑦) = (((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦))
64	63	fveq2d 6920	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → (𝐹‘(𝑥 “ 𝑦)) = (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)))
65	62, 64	mpteq12dv 5198	. . . . . . . . . . . . 13 ⊢ (𝑥 = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))) = (𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦))))
66	60	dmex 7955	. . . . . . . . . . . . . . 15 ⊢ dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ∈ V
67	66	pwex 5349	. . . . . . . . . . . . . 14 ⊢ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ∈ V
68	67	mptex 7260	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦))) ∈ V
69	65, 33, 68	fvmpt 7024	. . . . . . . . . . . 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 6917	. . . . . . . . . 10 ⊢ ((𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))‘𝑐) = ((𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)))‘𝑐)
72		r1sssuc 9827	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ On → (𝑅1‘𝑏) ⊆ (𝑅1‘suc 𝑏))
73	50, 72	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ ω → (𝑅1‘𝑏) ⊆ (𝑅1‘suc 𝑏))
74		fnssres 6692	. . . . . . . . . . . . . . . 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 6674	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ ω → dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) = (𝑅1‘𝑏))
77	76	pweqd 4577	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ ω → 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) = 𝒫 (𝑅1‘𝑏))
78	77	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) = 𝒫 (𝑅1‘𝑏))
79	54, 78	eleqtrrd 2867	. . . . . . . . . . 11 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝑐 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))
80		imaeq2 6066	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑐 → (((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦) = (((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐))
81	80	fveq2d 6920	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑐 → (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)) = (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐)))
82		eqid 2763	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦))) = (𝑦 ∈ 𝒫 dom ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) ↦ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑦)))
83		fvex 6929	. . . . . . . . . . . 12 ⊢ (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐)) ∈ V
84	81, 82, 83	fvmpt 7024	. . . . . . . . . . 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 2810	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)))‘𝑐) = (𝐹‘(((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) “ 𝑐)))
87		dmeq 5897	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (rec(𝐺, ∅)‘suc 𝑏) → dom 𝑥 = dom (rec(𝐺, ∅)‘suc 𝑏))
88	87	pweqd 4577	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (rec(𝐺, ∅)‘suc 𝑏) → 𝒫 dom 𝑥 = 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏))
89		imaeq1 6065	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (rec(𝐺, ∅)‘suc 𝑏) → (𝑥 “ 𝑦) = ((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦))
90	89	fveq2d 6920	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (rec(𝐺, ∅)‘suc 𝑏) → (𝐹‘(𝑥 “ 𝑦)) = (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)))
91	88, 90	mpteq12dv 5198	. . . . . . . . . . . . 13 ⊢ (𝑥 = (rec(𝐺, ∅)‘suc 𝑏) → (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦))))
92	59	dmex 7955	. . . . . . . . . . . . . . 15 ⊢ dom (rec(𝐺, ∅)‘suc 𝑏) ∈ V
93	92	pwex 5349	. . . . . . . . . . . . . 14 ⊢ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ∈ V
94	93	mptex 7260	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦))) ∈ V
95	91, 33, 94	fvmpt 7024	. . . . . . . . . . . 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 6917	. . . . . . . . . 10 ⊢ ((𝐺‘(rec(𝐺, ∅)‘suc 𝑏))‘𝑐) = ((𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)))‘𝑐)
98		r1tr 9820	. . . . . . . . . . . . . . 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 221	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ ω → (𝑅1‘suc 𝑏) ⊆ 𝒫 (𝑅1‘suc 𝑏))
102	101	sselda 3913	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝑐 ∈ 𝒫 (𝑅1‘suc 𝑏))
103		f1odm 6858	. . . . . . . . . . . . . . 15 ⊢ ((rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)⟶1-1onto(card‘(𝑅1‘suc 𝑏)) → dom (rec(𝐺, ∅)‘suc 𝑏) = (𝑅1‘suc 𝑏))
104	35, 103	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ ω → dom (rec(𝐺, ∅)‘suc 𝑏) = (𝑅1‘suc 𝑏))
105	104	pweqd 4577	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ ω → 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) = 𝒫 (𝑅1‘suc 𝑏))
106	105	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) = 𝒫 (𝑅1‘suc 𝑏))
107	102, 106	eleqtrrd 2867	. . . . . . . . . . 11 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → 𝑐 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏))
108		imaeq2 6066	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑐 → ((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦) = ((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐))
109	108	fveq2d 6920	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑐 → (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)) = (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐)))
110		eqid 2763	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦))) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘suc 𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑦)))
111		fvex 6929	. . . . . . . . . . . 12 ⊢ (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐)) ∈ V
112	109, 110, 111	fvmpt 7024	. . . . . . . . . . 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 2810	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((𝐺‘(rec(𝐺, ∅)‘suc 𝑏))‘𝑐) = (𝐹‘((rec(𝐺, ∅)‘suc 𝑏) “ 𝑐)))
115	58, 86, 114	3eqtr4d 2808	. . . . . . . 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 6916	. . . . . . . . 9 ⊢ ((rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏)) → (𝐺‘(rec(𝐺, ∅)‘𝑏)) = (𝐺‘((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))))
118	117	fveq1d 6918	. . . . . . . 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 8470	. . . . . . . . . 10 ⊢ (suc 𝑏 ∈ On → (rec(𝐺, ∅)‘suc suc 𝑏) = (𝐺‘(rec(𝐺, ∅)‘suc 𝑏)))
121	44, 120	syl 18	. . . . . . . . 9 ⊢ (𝑏 ∈ ω → (rec(𝐺, ∅)‘suc suc 𝑏) = (𝐺‘(rec(𝐺, ∅)‘suc 𝑏)))
122	121	fveq1d 6918	. . . . . . . 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 2809	. . . . . 6 ⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((rec(𝐺, ∅)‘suc suc 𝑏)‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘𝑏))‘𝑐))
125		fvres 6935	. . . . . . 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 8470	. . . . . . . . 9 ⊢ (𝑏 ∈ On → (rec(𝐺, ∅)‘suc 𝑏) = (𝐺‘(rec(𝐺, ∅)‘𝑏)))
128	50, 127	syl 18	. . . . . . . 8 ⊢ (𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏) = (𝐺‘(rec(𝐺, ∅)‘𝑏)))
129	128	fveq1d 6918	. . . . . . 7 ⊢ (𝑏 ∈ ω → ((rec(𝐺, ∅)‘suc 𝑏)‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘𝑏))‘𝑐))
130	129	ad2antrr 739	. . . . . 6 ⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((rec(𝐺, ∅)‘suc 𝑏)‘𝑐) = ((𝐺‘(rec(𝐺, ∅)‘𝑏))‘𝑐))
131	124, 126, 130	3eqtr4rd 2809	. . . . 5 ⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏) = ((rec(𝐺, ∅)‘suc 𝑏) ↾ (𝑅1‘𝑏))) ∧ 𝑐 ∈ (𝑅1‘suc 𝑏)) → ((rec(𝐺, ∅)‘suc 𝑏)‘𝑐) = (((rec(𝐺, ∅)‘suc suc 𝑏) ↾ (𝑅1‘suc 𝑏))‘𝑐))
132	38, 49, 131	eqfnfvd 7063	. . . 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 7942	. 2 ⊢ (𝐴 ∈ ω → (rec(𝐺, ∅)‘𝐴) = ((rec(𝐺, ∅)‘suc 𝐴) ↾ (𝑅1‘𝐴)))
135		resss 6008	. 2 ⊢ ((rec(𝐺, ∅)‘suc 𝐴) ↾ (𝑅1‘𝐴)) ⊆ (rec(𝐺, ∅)‘suc 𝐴)
136	134, 135	eqsstrdi 3957	1 ⊢ (𝐴 ∈ ω → (rec(𝐺, ∅)‘𝐴) ⊆ (rec(𝐺, ∅)‘suc 𝐴))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  Vcvv 3454   ⊆ wss 3900   ∩ cin 4092  ∅c0 4281  𝒫 cpw 4560  {csn 4588  ∪ ciun 4956   ↦ cmpt 5192  Tr wtr 5218   × cxp 5656  dom cdm 5658   ↾ cres 5660   “ cima 5661  Oncon0 6388  suc csuc 6390   Fn wfn 6561  ⟶1-1ontowf1o 6565  ‘cfv 6566  ωcom 7911  reccrdg 8455  Fincfn 9011  𝑅₁cr1 9803  cardccrd 10053

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5238  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-int 4913  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-ov 7454  df-oprab 7455  df-mpo 7456  df-om 7912  df-1st 8035  df-2nd 8036  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-1o 8514  df-2o 8515  df-oadd 8518  df-er 8755  df-map 8887  df-en 9012  df-dom 9013  df-sdom 9014  df-fin 9015  df-r1 9805  df-dju 10019  df-card 10057

This theorem is used by:  ackbij2lem4  10358