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 fndm ⊢ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) Fn ( 𝑅1 ‘ 𝑏 ) → dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) = ( 𝑅1 ‘ 𝑏 ) )
77 75 76 syl ⊢ ( 𝑏 ∈ ω → dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) = ( 𝑅1 ‘ 𝑏 ) )
78 77 pweqd ⊢ ( 𝑏 ∈ ω → 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) = 𝒫 ( 𝑅1 ‘ 𝑏 ) )
79 78 adantr ⊢ ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) = 𝒫 ( 𝑅1 ‘ 𝑏 ) )
80 54 79 eleqtrrd ⊢ ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → 𝑐 ∈ 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) )
81 imaeq2 ⊢ ( 𝑦 = 𝑐 → ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑦 ) = ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑐 ) )
82 81 fveq2d ⊢ ( 𝑦 = 𝑐 → ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑦 ) ) = ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑐 ) ) )
83 eqid ⊢ ( 𝑦 ∈ 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ↦ ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑦 ) ) ) = ( 𝑦 ∈ 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ↦ ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑦 ) ) )
84 fvex ⊢ ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑐 ) ) ∈ V
85 82 83 84 fvmpt ⊢ ( 𝑐 ∈ 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) → ( ( 𝑦 ∈ 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ↦ ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑦 ) ) ) ‘ 𝑐 ) = ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑐 ) ) )
86 80 85 syl ⊢ ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( 𝑦 ∈ 𝒫 dom ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ↦ ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑦 ) ) ) ‘ 𝑐 ) = ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑐 ) ) )
87 71 86 syl5eq ⊢ ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( 𝐺 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) ‘ 𝑐 ) = ( 𝐹 ‘ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) “ 𝑐 ) ) )
88 dmeq ⊢ ( 𝑥 = ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) → dom 𝑥 = dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) )
89 88 pweqd ⊢ ( 𝑥 = ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) → 𝒫 dom 𝑥 = 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) )
90 imaeq1 ⊢ ( 𝑥 = ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) → ( 𝑥 “ 𝑦 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) )
91 90 fveq2d ⊢ ( 𝑥 = ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) → ( 𝐹 ‘ ( 𝑥 “ 𝑦 ) ) = ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) )
92 89 91 mpteq12dv ⊢ ( 𝑥 = ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) → ( 𝑦 ∈ 𝒫 dom 𝑥 ↦ ( 𝐹 ‘ ( 𝑥 “ 𝑦 ) ) ) = ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) ) )
93 59 dmex ⊢ dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ∈ V
94 93 pwex ⊢ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ∈ V
95 94 mptex ⊢ ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) ) ∈ V
96 92 2 95 fvmpt ⊢ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ∈ V → ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) = ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) ) )
97 59 96 ax-mp ⊢ ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) = ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) )
98 97 fveq1i ⊢ ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) ‘ 𝑐 ) = ( ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) ) ‘ 𝑐 )
99 r1tr ⊢ Tr ( 𝑅1 ‘ suc 𝑏 )
100 99 a1i ⊢ ( 𝑏 ∈ ω → Tr ( 𝑅1 ‘ suc 𝑏 ) )
101 dftr4 ⊢ ( Tr ( 𝑅1 ‘ suc 𝑏 ) ↔ ( 𝑅1 ‘ suc 𝑏 ) ⊆ 𝒫 ( 𝑅1 ‘ suc 𝑏 ) )
102 100 101 sylib ⊢ ( 𝑏 ∈ ω → ( 𝑅1 ‘ suc 𝑏 ) ⊆ 𝒫 ( 𝑅1 ‘ suc 𝑏 ) )
103 102 sselda ⊢ ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → 𝑐 ∈ 𝒫 ( 𝑅1 ‘ suc 𝑏 ) )
104 f1odm ⊢ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) : ( 𝑅1 ‘ suc 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) → dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = ( 𝑅1 ‘ suc 𝑏 ) )
105 35 104 syl ⊢ ( 𝑏 ∈ ω → dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = ( 𝑅1 ‘ suc 𝑏 ) )
106 105 pweqd ⊢ ( 𝑏 ∈ ω → 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = 𝒫 ( 𝑅1 ‘ suc 𝑏 ) )
107 106 adantr ⊢ ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = 𝒫 ( 𝑅1 ‘ suc 𝑏 ) )
108 103 107 eleqtrrd ⊢ ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → 𝑐 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) )
109 imaeq2 ⊢ ( 𝑦 = 𝑐 → ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑐 ) )
110 109 fveq2d ⊢ ( 𝑦 = 𝑐 → ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) = ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑐 ) ) )
111 eqid ⊢ ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) ) = ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) )
112 fvex ⊢ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑐 ) ) ∈ V
113 110 111 112 fvmpt ⊢ ( 𝑐 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) → ( ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) ) ‘ 𝑐 ) = ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑐 ) ) )
114 108 113 syl ⊢ ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑦 ) ) ) ‘ 𝑐 ) = ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑐 ) ) )
115 98 114 syl5eq ⊢ ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) ‘ 𝑐 ) = ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) “ 𝑐 ) ) )
116 58 87 115 3eqtr4d ⊢ ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( 𝐺 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) ‘ 𝑐 ) = ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) ‘ 𝑐 ) )
117 116 adantlr ⊢ ( ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( 𝐺 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) ‘ 𝑐 ) = ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) ‘ 𝑐 ) )
118 fveq2 ⊢ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) → ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ) = ( 𝐺 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) )
119 118 fveq1d ⊢ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) → ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ) ‘ 𝑐 ) = ( ( 𝐺 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) ‘ 𝑐 ) )
120 119 ad2antlr ⊢ ( ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ) ‘ 𝑐 ) = ( ( 𝐺 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) ‘ 𝑐 ) )
121 rdgsuc ⊢ ( suc 𝑏 ∈ On → ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) = ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) )
122 44 121 syl ⊢ ( 𝑏 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) = ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) )
123 122 fveq1d ⊢ ( 𝑏 ∈ ω → ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ‘ 𝑐 ) = ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) ‘ 𝑐 ) )
124 123 ad2antrr ⊢ ( ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ‘ 𝑐 ) = ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) ‘ 𝑐 ) )
125 117 120 124 3eqtr4rd ⊢ ( ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ‘ 𝑐 ) = ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ) ‘ 𝑐 ) )
126 fvres ⊢ ( 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) → ( ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ↾ ( 𝑅1 ‘ suc 𝑏 ) ) ‘ 𝑐 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ‘ 𝑐 ) )
127 126 adantl ⊢ ( ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ↾ ( 𝑅1 ‘ suc 𝑏 ) ) ‘ 𝑐 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ‘ 𝑐 ) )
128 rdgsuc ⊢ ( 𝑏 ∈ On → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ) )
129 50 128 syl ⊢ ( 𝑏 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ) )
130 129 fveq1d ⊢ ( 𝑏 ∈ ω → ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ‘ 𝑐 ) = ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ) ‘ 𝑐 ) )
131 130 ad2antrr ⊢ ( ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ‘ 𝑐 ) = ( ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ) ‘ 𝑐 ) )
132 125 127 131 3eqtr4rd ⊢ ( ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) ∧ 𝑐 ∈ ( 𝑅1 ‘ suc 𝑏 ) ) → ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ‘ 𝑐 ) = ( ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ↾ ( 𝑅1 ‘ suc 𝑏 ) ) ‘ 𝑐 ) )
133 38 49 132 eqfnfvd ⊢ ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) ) → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ↾ ( 𝑅1 ‘ suc 𝑏 ) ) )
134 133 ex ⊢ ( 𝑏 ∈ ω → ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ↾ ( 𝑅1 ‘ 𝑏 ) ) → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc suc 𝑏 ) ↾ ( 𝑅1 ‘ suc 𝑏 ) ) ) )
135 8 14 20 26 32 134 finds ⊢ ( 𝐴 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ 𝐴 ) = ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝐴 ) ↾ ( 𝑅1 ‘ 𝐴 ) ) )
136 resss ⊢ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝐴 ) ↾ ( 𝑅1 ‘ 𝐴 ) ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ suc 𝐴 )
137 135 136 eqsstrdi ⊢ ( 𝐴 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ 𝐴 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ suc 𝐴 ) )