Metamath Proof Explorer


Theorem ackbij2lem3

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

Ref Expression
Hypotheses ackbij.f 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ 𝑦𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
ackbij.g 𝐺 = ( 𝑥 ∈ V ↦ ( 𝑦 ∈ 𝒫 dom 𝑥 ↦ ( 𝐹 ‘ ( 𝑥𝑦 ) ) ) )
Assertion ackbij2lem3 ( 𝐴 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ 𝐴 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ suc 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ackbij.f 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ 𝑦𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
2 ackbij.g 𝐺 = ( 𝑥 ∈ V ↦ ( 𝑦 ∈ 𝒫 dom 𝑥 ↦ ( 𝐹 ‘ ( 𝑥𝑦 ) ) ) )
3 fveq2 ( 𝑎 = ∅ → ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) = ( rec ( 𝐺 , ∅ ) ‘ ∅ ) )
4 suceq ( 𝑎 = ∅ → suc 𝑎 = suc ∅ )
5 4 fveq2d ( 𝑎 = ∅ → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑎 ) = ( rec ( 𝐺 , ∅ ) ‘ suc ∅ ) )
6 fveq2 ( 𝑎 = ∅ → ( 𝑅1𝑎 ) = ( 𝑅1 ‘ ∅ ) )
7 5 6 reseq12d ( 𝑎 = ∅ → ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑎 ) ↾ ( 𝑅1𝑎 ) ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc ∅ ) ↾ ( 𝑅1 ‘ ∅ ) ) )
8 3 7 eqeq12d ( 𝑎 = ∅ → ( ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑎 ) ↾ ( 𝑅1𝑎 ) ) ↔ ( rec ( 𝐺 , ∅ ) ‘ ∅ ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc ∅ ) ↾ ( 𝑅1 ‘ ∅ ) ) ) )
9 fveq2 ( 𝑎 = 𝑏 → ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) = ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) )
10 suceq ( 𝑎 = 𝑏 → suc 𝑎 = suc 𝑏 )
11 10 fveq2d ( 𝑎 = 𝑏 → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑎 ) = ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) )
12 fveq2 ( 𝑎 = 𝑏 → ( 𝑅1𝑎 ) = ( 𝑅1𝑏 ) )
13 11 12 reseq12d ( 𝑎 = 𝑏 → ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑎 ) ↾ ( 𝑅1𝑎 ) ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) )
14 9 13 eqeq12d ( 𝑎 = 𝑏 → ( ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑎 ) ↾ ( 𝑅1𝑎 ) ) ↔ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ) )
15 fveq2 ( 𝑎 = suc 𝑏 → ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) = ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) )
16 suceq ( 𝑎 = suc 𝑏 → suc 𝑎 = suc suc 𝑏 )
17 16 fveq2d ( 𝑎 = suc 𝑏 → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑎 ) = ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) )
18 fveq2 ( 𝑎 = suc 𝑏 → ( 𝑅1𝑎 ) = ( 𝑅1 ‘ suc 𝑏 ) )
19 17 18 reseq12d ( 𝑎 = suc 𝑏 → ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑎 ) ↾ ( 𝑅1𝑎 ) ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ↾ ( 𝑅1 ‘ suc 𝑏 ) ) )
20 15 19 eqeq12d ( 𝑎 = suc 𝑏 → ( ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑎 ) ↾ ( 𝑅1𝑎 ) ) ↔ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ↾ ( 𝑅1 ‘ suc 𝑏 ) ) ) )
21 fveq2 ( 𝑎 = 𝐴 → ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) = ( rec ( 𝐺 , ∅ ) ‘ 𝐴 ) )
22 suceq ( 𝑎 = 𝐴 → suc 𝑎 = suc 𝐴 )
23 22 fveq2d ( 𝑎 = 𝐴 → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑎 ) = ( rec ( 𝐺 , ∅ ) ‘ suc 𝐴 ) )
24 fveq2 ( 𝑎 = 𝐴 → ( 𝑅1𝑎 ) = ( 𝑅1𝐴 ) )
25 23 24 reseq12d ( 𝑎 = 𝐴 → ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑎 ) ↾ ( 𝑅1𝑎 ) ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝐴 ) ↾ ( 𝑅1𝐴 ) ) )
26 21 25 eqeq12d ( 𝑎 = 𝐴 → ( ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑎 ) ↾ ( 𝑅1𝑎 ) ) ↔ ( rec ( 𝐺 , ∅ ) ‘ 𝐴 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝐴 ) ↾ ( 𝑅1𝐴 ) ) ) )
27 res0 ( ( rec ( 𝐺 , ∅ ) ‘ suc ∅ ) ↾ ∅ ) = ∅
28 r10 ( 𝑅1 ‘ ∅ ) = ∅
29 28 reseq2i ( ( rec ( 𝐺 , ∅ ) ‘ suc ∅ ) ↾ ( 𝑅1 ‘ ∅ ) ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc ∅ ) ↾ ∅ )
30 0ex ∅ ∈ V
31 30 rdg0 ( rec ( 𝐺 , ∅ ) ‘ ∅ ) = ∅
32 27 29 31 3eqtr4ri ( rec ( 𝐺 , ∅ ) ‘ ∅ ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc ∅ ) ↾ ( 𝑅1 ‘ ∅ ) )
33 peano2 ( 𝑏 ∈ ω → suc 𝑏 ∈ ω )
34 1 2 ackbij2lem2 ( suc 𝑏 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) : ( 𝑅1 ‘ suc 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) )
35 33 34 syl ( 𝑏 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) : ( 𝑅1 ‘ suc 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) )
36 f1ofn ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) : ( 𝑅1 ‘ suc 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) Fn ( 𝑅1 ‘ suc 𝑏 ) )
37 35 36 syl ( 𝑏 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) Fn ( 𝑅1 ‘ suc 𝑏 ) )
38 37 adantr ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ) → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) Fn ( 𝑅1 ‘ suc 𝑏 ) )
39 peano2 ( suc 𝑏 ∈ ω → suc suc 𝑏 ∈ ω )
40 1 2 ackbij2lem2 ( suc suc 𝑏 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) : ( 𝑅1 ‘ suc suc 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ suc suc 𝑏 ) ) )
41 f1ofn ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) : ( 𝑅1 ‘ suc suc 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ suc suc 𝑏 ) ) → ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) Fn ( 𝑅1 ‘ suc suc 𝑏 ) )
42 33 39 40 41 4syl ( 𝑏 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) Fn ( 𝑅1 ‘ suc suc 𝑏 ) )
43 nnon ( suc 𝑏 ∈ ω → suc 𝑏 ∈ On )
44 33 43 syl ( 𝑏 ∈ ω → suc 𝑏 ∈ On )
45 r1sssuc ( suc 𝑏 ∈ On → ( 𝑅1 ‘ suc 𝑏 ) ⊆ ( 𝑅1 ‘ suc suc 𝑏 ) )
46 44 45 syl ( 𝑏 ∈ ω → ( 𝑅1 ‘ suc 𝑏 ) ⊆ ( 𝑅1 ‘ suc suc 𝑏 ) )
47 fnssres ( ( ( 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 ( 𝑏 ∈ ω → ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ↾ ( 𝑅1 ‘ suc 𝑏 ) ) Fn ( 𝑅1 ‘ suc 𝑏 ) )
49 48 adantr ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ) → ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ↾ ( 𝑅1 ‘ suc 𝑏 ) ) Fn ( 𝑅1 ‘ suc 𝑏 ) )
50 nnon ( 𝑏 ∈ ω → 𝑏 ∈ On )
51 r1suc ( 𝑏 ∈ On → ( 𝑅1 ‘ suc 𝑏 ) = 𝒫 ( 𝑅1𝑏 ) )
52 50 51 syl ( 𝑏 ∈ ω → ( 𝑅1 ‘ suc 𝑏 ) = 𝒫 ( 𝑅1𝑏 ) )
53 52 eleq2d ( 𝑏 ∈ ω → ( 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ↔ 𝑐 ∈ 𝒫 ( 𝑅1𝑏 ) ) )
54 53 biimpa ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → 𝑐 ∈ 𝒫 ( 𝑅1𝑏 ) )
55 54 elpwid ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → 𝑐 ⊆ ( 𝑅1𝑏 ) )
56 resima2 ( 𝑐 ⊆ ( 𝑅1𝑏 ) → ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) “ 𝑐 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑐 ) )
57 55 56 syl ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) “ 𝑐 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑐 ) )
58 57 fveq2d ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) “ 𝑐 ) ) = ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑐 ) ) )
59 fvex ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ∈ V
60 59 resex ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ∈ V
61 dmeq ( 𝑥 = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) → dom 𝑥 = dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) )
62 61 pweqd ( 𝑥 = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) → 𝒫 dom 𝑥 = 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) )
63 imaeq1 ( 𝑥 = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) → ( 𝑥𝑦 ) = ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) “ 𝑦 ) )
64 63 fveq2d ( 𝑥 = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) → ( 𝐹 ‘ ( 𝑥𝑦 ) ) = ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) “ 𝑦 ) ) )
65 62 64 mpteq12dv ( 𝑥 = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) → ( 𝑦 ∈ 𝒫 dom 𝑥 ↦ ( 𝐹 ‘ ( 𝑥𝑦 ) ) ) = ( 𝑦 ∈ 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ↦ ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) “ 𝑦 ) ) ) )
66 60 dmex dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ∈ V
67 66 pwex 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ∈ V
68 67 mptex ( 𝑦 ∈ 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ↦ ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) “ 𝑦 ) ) ) ∈ V
69 65 2 68 fvmpt ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ∈ V → ( 𝐺 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ) = ( 𝑦 ∈ 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ↦ ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) “ 𝑦 ) ) ) )
70 60 69 ax-mp ( 𝐺 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ) = ( 𝑦 ∈ 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ↦ ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) “ 𝑦 ) ) )
71 70 fveq1i ( ( 𝐺 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ) ‘ 𝑐 ) = ( ( 𝑦 ∈ 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ↦ ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) “ 𝑦 ) ) ) ‘ 𝑐 )
72 r1sssuc ( 𝑏 ∈ On → ( 𝑅1𝑏 ) ⊆ ( 𝑅1 ‘ suc 𝑏 ) )
73 50 72 syl ( 𝑏 ∈ ω → ( 𝑅1𝑏 ) ⊆ ( 𝑅1 ‘ suc 𝑏 ) )
74 fnssres ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) Fn ( 𝑅1 ‘ suc 𝑏 ) ∧ ( 𝑅1𝑏 ) ⊆ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) Fn ( 𝑅1𝑏 ) )
75 37 73 74 syl2anc ( 𝑏 ∈ ω → ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) Fn ( 𝑅1𝑏 ) )
76 75 fndmd ( 𝑏 ∈ ω → dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) = ( 𝑅1𝑏 ) )
77 76 pweqd ( 𝑏 ∈ ω → 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) = 𝒫 ( 𝑅1𝑏 ) )
78 77 adantr ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) = 𝒫 ( 𝑅1𝑏 ) )
79 54 78 eleqtrrd ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → 𝑐 ∈ 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) )
80 imaeq2 ( 𝑦 = 𝑐 → ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) “ 𝑦 ) = ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) “ 𝑐 ) )
81 80 fveq2d ( 𝑦 = 𝑐 → ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) “ 𝑦 ) ) = ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) “ 𝑐 ) ) )
82 eqid ( 𝑦 ∈ 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ↦ ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) “ 𝑦 ) ) ) = ( 𝑦 ∈ 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ↦ ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) “ 𝑦 ) ) )
83 fvex ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) “ 𝑐 ) ) ∈ V
84 81 82 83 fvmpt ( 𝑐 ∈ 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) → ( ( 𝑦 ∈ 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ↦ ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) “ 𝑦 ) ) ) ‘ 𝑐 ) = ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) “ 𝑐 ) ) )
85 79 84 syl ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( 𝑦 ∈ 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ↦ ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) “ 𝑦 ) ) ) ‘ 𝑐 ) = ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) “ 𝑐 ) ) )
86 71 85 eqtrid ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( 𝐺 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ) ‘ 𝑐 ) = ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) “ 𝑐 ) ) )
87 dmeq ( 𝑥 = ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) → dom 𝑥 = dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) )
88 87 pweqd ( 𝑥 = ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) → 𝒫 dom 𝑥 = 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) )
89 imaeq1 ( 𝑥 = ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) → ( 𝑥𝑦 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) )
90 89 fveq2d ( 𝑥 = ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) → ( 𝐹 ‘ ( 𝑥𝑦 ) ) = ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) )
91 88 90 mpteq12dv ( 𝑥 = ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) → ( 𝑦 ∈ 𝒫 dom 𝑥 ↦ ( 𝐹 ‘ ( 𝑥𝑦 ) ) ) = ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) ) )
92 59 dmex dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ∈ V
93 92 pwex 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ∈ V
94 93 mptex ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) ) ∈ V
95 91 2 94 fvmpt ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ∈ V → ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) = ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) ) )
96 59 95 ax-mp ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) = ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) )
97 96 fveq1i ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) ‘ 𝑐 ) = ( ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) ) ‘ 𝑐 )
98 r1tr Tr ( 𝑅1 ‘ suc 𝑏 )
99 98 a1i ( 𝑏 ∈ ω → Tr ( 𝑅1 ‘ suc 𝑏 ) )
100 dftr4 ( Tr ( 𝑅1 ‘ suc 𝑏 ) ↔ ( 𝑅1 ‘ suc 𝑏 ) ⊆ 𝒫 ( 𝑅1 ‘ suc 𝑏 ) )
101 99 100 sylib ( 𝑏 ∈ ω → ( 𝑅1 ‘ suc 𝑏 ) ⊆ 𝒫 ( 𝑅1 ‘ suc 𝑏 ) )
102 101 sselda ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → 𝑐 ∈ 𝒫 ( 𝑅1 ‘ suc 𝑏 ) )
103 f1odm ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) : ( 𝑅1 ‘ suc 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) → dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = ( 𝑅1 ‘ suc 𝑏 ) )
104 35 103 syl ( 𝑏 ∈ ω → dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = ( 𝑅1 ‘ suc 𝑏 ) )
105 104 pweqd ( 𝑏 ∈ ω → 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = 𝒫 ( 𝑅1 ‘ suc 𝑏 ) )
106 105 adantr ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = 𝒫 ( 𝑅1 ‘ suc 𝑏 ) )
107 102 106 eleqtrrd ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → 𝑐 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) )
108 imaeq2 ( 𝑦 = 𝑐 → ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑐 ) )
109 108 fveq2d ( 𝑦 = 𝑐 → ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) = ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑐 ) ) )
110 eqid ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) ) = ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) )
111 fvex ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑐 ) ) ∈ V
112 109 110 111 fvmpt ( 𝑐 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) → ( ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) ) ‘ 𝑐 ) = ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑐 ) ) )
113 107 112 syl ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) ) ‘ 𝑐 ) = ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑐 ) ) )
114 97 113 eqtrid ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) ‘ 𝑐 ) = ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑐 ) ) )
115 58 86 114 3eqtr4d ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( 𝐺 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ) ‘ 𝑐 ) = ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) ‘ 𝑐 ) )
116 115 adantlr ( ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ) ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( 𝐺 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ) ‘ 𝑐 ) = ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) ‘ 𝑐 ) )
117 fveq2 ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) → ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ) = ( 𝐺 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ) )
118 117 fveq1d ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) → ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ) ‘ 𝑐 ) = ( ( 𝐺 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ) ‘ 𝑐 ) )
119 118 ad2antlr ( ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ) ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ) ‘ 𝑐 ) = ( ( 𝐺 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ) ‘ 𝑐 ) )
120 rdgsuc ( suc 𝑏 ∈ On → ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) = ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) )
121 44 120 syl ( 𝑏 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) = ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) )
122 121 fveq1d ( 𝑏 ∈ ω → ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ‘ 𝑐 ) = ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) ‘ 𝑐 ) )
123 122 ad2antrr ( ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ) ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ‘ 𝑐 ) = ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) ‘ 𝑐 ) )
124 116 119 123 3eqtr4rd ( ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ) ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ‘ 𝑐 ) = ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ) ‘ 𝑐 ) )
125 fvres ( 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) → ( ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ↾ ( 𝑅1 ‘ suc 𝑏 ) ) ‘ 𝑐 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ‘ 𝑐 ) )
126 125 adantl ( ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ) ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ↾ ( 𝑅1 ‘ suc 𝑏 ) ) ‘ 𝑐 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ‘ 𝑐 ) )
127 rdgsuc ( 𝑏 ∈ On → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ) )
128 50 127 syl ( 𝑏 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ) )
129 128 fveq1d ( 𝑏 ∈ ω → ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ‘ 𝑐 ) = ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ) ‘ 𝑐 ) )
130 129 ad2antrr ( ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ) ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ‘ 𝑐 ) = ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ) ‘ 𝑐 ) )
131 124 126 130 3eqtr4rd ( ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ) ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ‘ 𝑐 ) = ( ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ↾ ( 𝑅1 ‘ suc 𝑏 ) ) ‘ 𝑐 ) )
132 38 49 131 eqfnfvd ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) ) → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ↾ ( 𝑅1 ‘ suc 𝑏 ) ) )
133 132 ex ( 𝑏 ∈ ω → ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1𝑏 ) ) → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ↾ ( 𝑅1 ‘ suc 𝑏 ) ) ) )
134 8 14 20 26 32 133 finds ( 𝐴 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ 𝐴 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝐴 ) ↾ ( 𝑅1𝐴 ) ) )
135 resss ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝐴 ) ↾ ( 𝑅1𝐴 ) ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ suc 𝐴 )
136 134 135 eqsstrdi ( 𝐴 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ 𝐴 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ suc 𝐴 ) )