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 𝐴 ) )