Metamath Proof Explorer

Theorem ackbij2lem2

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

Ref Expression
Hypotheses ackbij.f ⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
ackbij.g ⊢ 𝐺 = ( 𝑥 ∈ V ↦ ( 𝑦 ∈ 𝒫 dom 𝑥 ↦ ( 𝐹 ‘ ( 𝑥 “ 𝑦 ) ) ) )
Assertion ackbij2lem2 ( 𝐴 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ 𝐴 ) : ( 𝑅1 ‘ 𝐴 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 ackbij.f ⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
2 ackbij.g ⊢ 𝐺 = ( 𝑥 ∈ V ↦ ( 𝑦 ∈ 𝒫 dom 𝑥 ↦ ( 𝐹 ‘ ( 𝑥 “ 𝑦 ) ) ) )
3 fveq2 ⊢ ( 𝑎 = ∅ → ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) = ( rec ( 𝐺 , ∅ ) ‘ ∅ ) )
4 fveq2 ⊢ ( 𝑎 = ∅ → ( 𝑅1 ‘ 𝑎 ) = ( 𝑅1 ‘ ∅ ) )
5 2fveq3 ⊢ ( 𝑎 = ∅ → ( card ‘ ( 𝑅1 ‘ 𝑎 ) ) = ( card ‘ ( 𝑅1 ‘ ∅ ) ) )
6 3 4 5 f1oeq123d ⊢ ( 𝑎 = ∅ → ( ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) : ( 𝑅1 ‘ 𝑎 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑎 ) ) ↔ ( rec ( 𝐺 , ∅ ) ‘ ∅ ) : ( 𝑅1 ‘ ∅ ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ ∅ ) ) ) )
7 fveq2 ⊢ ( 𝑎 = 𝑏 → ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) = ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) )
8 fveq2 ⊢ ( 𝑎 = 𝑏 → ( 𝑅1 ‘ 𝑎 ) = ( 𝑅1 ‘ 𝑏 ) )
9 2fveq3 ⊢ ( 𝑎 = 𝑏 → ( card ‘ ( 𝑅1 ‘ 𝑎 ) ) = ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) )
10 7 8 9 f1oeq123d ⊢ ( 𝑎 = 𝑏 → ( ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) : ( 𝑅1 ‘ 𝑎 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑎 ) ) ↔ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) : ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) )
11 fveq2 ⊢ ( 𝑎 = suc 𝑏 → ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) = ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) )
12 fveq2 ⊢ ( 𝑎 = suc 𝑏 → ( 𝑅1 ‘ 𝑎 ) = ( 𝑅1 ‘ suc 𝑏 ) )
13 2fveq3 ⊢ ( 𝑎 = suc 𝑏 → ( card ‘ ( 𝑅1 ‘ 𝑎 ) ) = ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) )
14 11 12 13 f1oeq123d ⊢ ( 𝑎 = suc 𝑏 → ( ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) : ( 𝑅1 ‘ 𝑎 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑎 ) ) ↔ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) : ( 𝑅1 ‘ suc 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) ) )
15 fveq2 ⊢ ( 𝑎 = 𝐴 → ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) = ( rec ( 𝐺 , ∅ ) ‘ 𝐴 ) )
16 fveq2 ⊢ ( 𝑎 = 𝐴 → ( 𝑅1 ‘ 𝑎 ) = ( 𝑅1 ‘ 𝐴 ) )
17 2fveq3 ⊢ ( 𝑎 = 𝐴 → ( card ‘ ( 𝑅1 ‘ 𝑎 ) ) = ( card ‘ ( 𝑅1 ‘ 𝐴 ) ) )
18 15 16 17 f1oeq123d ⊢ ( 𝑎 = 𝐴 → ( ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) : ( 𝑅1 ‘ 𝑎 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑎 ) ) ↔ ( rec ( 𝐺 , ∅ ) ‘ 𝐴 ) : ( 𝑅1 ‘ 𝐴 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝐴 ) ) ) )
19 f1o0 ⊢ ∅ : ∅ –1-1-onto→ ∅
20 0ex ⊢ ∅ ∈ V
21 20 rdg0 ⊢ ( rec ( 𝐺 , ∅ ) ‘ ∅ ) = ∅
22 f1oeq1 ⊢ ( ( rec ( 𝐺 , ∅ ) ‘ ∅ ) = ∅ → ( ( rec ( 𝐺 , ∅ ) ‘ ∅ ) : ( 𝑅1 ‘ ∅ ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ ∅ ) ) ↔ ∅ : ( 𝑅1 ‘ ∅ ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ ∅ ) ) ) )
23 21 22 ax-mp ⊢ ( ( rec ( 𝐺 , ∅ ) ‘ ∅ ) : ( 𝑅1 ‘ ∅ ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ ∅ ) ) ↔ ∅ : ( 𝑅1 ‘ ∅ ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ ∅ ) ) )
24 r10 ⊢ ( 𝑅1 ‘ ∅ ) = ∅
25 24 fveq2i ⊢ ( card ‘ ( 𝑅1 ‘ ∅ ) ) = ( card ‘ ∅ )
26 card0 ⊢ ( card ‘ ∅ ) = ∅
27 25 26 eqtri ⊢ ( card ‘ ( 𝑅1 ‘ ∅ ) ) = ∅
28 f1oeq23 ⊢ ( ( ( 𝑅1 ‘ ∅ ) = ∅ ∧ ( card ‘ ( 𝑅1 ‘ ∅ ) ) = ∅ ) → ( ∅ : ( 𝑅1 ‘ ∅ ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ ∅ ) ) ↔ ∅ : ∅ –1-1-onto→ ∅ ) )
29 24 27 28 mp2an ⊢ ( ∅ : ( 𝑅1 ‘ ∅ ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ ∅ ) ) ↔ ∅ : ∅ –1-1-onto→ ∅ )
30 23 29 bitri ⊢ ( ( rec ( 𝐺 , ∅ ) ‘ ∅ ) : ( 𝑅1 ‘ ∅ ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ ∅ ) ) ↔ ∅ : ∅ –1-1-onto→ ∅ )
31 19 30 mpbir ⊢ ( rec ( 𝐺 , ∅ ) ‘ ∅ ) : ( 𝑅1 ‘ ∅ ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ ∅ ) )
32 1 ackbij1lem17 ⊢ 𝐹 : ( 𝒫 ω ∩ Fin ) –1-1→ ω
33 32 a1i ⊢ ( 𝑏 ∈ ω → 𝐹 : ( 𝒫 ω ∩ Fin ) –1-1→ ω )
34 r1fin ⊢ ( 𝑏 ∈ ω → ( 𝑅1 ‘ 𝑏 ) ∈ Fin )
35 ficardom ⊢ ( ( 𝑅1 ‘ 𝑏 ) ∈ Fin → ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ∈ ω )
36 34 35 syl ⊢ ( 𝑏 ∈ ω → ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ∈ ω )
37 ackbij2lem1 ⊢ ( ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ∈ ω → 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ⊆ ( 𝒫 ω ∩ Fin ) )
38 36 37 syl ⊢ ( 𝑏 ∈ ω → 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ⊆ ( 𝒫 ω ∩ Fin ) )
39 f1ores ⊢ ( ( 𝐹 : ( 𝒫 ω ∩ Fin ) –1-1→ ω ∧ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ⊆ ( 𝒫 ω ∩ Fin ) ) → ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) : 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) –1-1-onto→ ( 𝐹 “ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) )
40 33 38 39 syl2anc ⊢ ( 𝑏 ∈ ω → ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) : 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) –1-1-onto→ ( 𝐹 “ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) )
41 1 ackbij1b ⊢ ( ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ∈ ω → ( 𝐹 “ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) = ( card ‘ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) )
42 36 41 syl ⊢ ( 𝑏 ∈ ω → ( 𝐹 “ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) = ( card ‘ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) )
43 ficardid ⊢ ( ( 𝑅1 ‘ 𝑏 ) ∈ Fin → ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ≈ ( 𝑅1 ‘ 𝑏 ) )
44 pwen ⊢ ( ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ≈ ( 𝑅1 ‘ 𝑏 ) → 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ≈ 𝒫 ( 𝑅1 ‘ 𝑏 ) )
45 carden2b ⊢ ( 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ≈ 𝒫 ( 𝑅1 ‘ 𝑏 ) → ( card ‘ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) = ( card ‘ 𝒫 ( 𝑅1 ‘ 𝑏 ) ) )
46 34 43 44 45 4syl ⊢ ( 𝑏 ∈ ω → ( card ‘ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) = ( card ‘ 𝒫 ( 𝑅1 ‘ 𝑏 ) ) )
47 42 46 eqtrd ⊢ ( 𝑏 ∈ ω → ( 𝐹 “ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) = ( card ‘ 𝒫 ( 𝑅1 ‘ 𝑏 ) ) )
48 47 f1oeq3d ⊢ ( 𝑏 ∈ ω → ( ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) : 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) –1-1-onto→ ( 𝐹 “ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ↔ ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) : 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) –1-1-onto→ ( card ‘ 𝒫 ( 𝑅1 ‘ 𝑏 ) ) ) )
49 40 48 mpbid ⊢ ( 𝑏 ∈ ω → ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) : 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) –1-1-onto→ ( card ‘ 𝒫 ( 𝑅1 ‘ 𝑏 ) ) )
50 49 adantr ⊢ ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) : ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) → ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) : 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) –1-1-onto→ ( card ‘ 𝒫 ( 𝑅1 ‘ 𝑏 ) ) )
51 f1opw ⊢ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) : ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) → ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) : 𝒫 ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) )
52 51 adantl ⊢ ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) : ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) → ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) : 𝒫 ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) )
53 f1oco ⊢ ( ( ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) : 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) –1-1-onto→ ( card ‘ 𝒫 ( 𝑅1 ‘ 𝑏 ) ) ∧ ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) : 𝒫 ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) → ( ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ∘ ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) ) : 𝒫 ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ 𝒫 ( 𝑅1 ‘ 𝑏 ) ) )
54 50 52 53 syl2anc ⊢ ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) : ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) → ( ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ∘ ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) ) : 𝒫 ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ 𝒫 ( 𝑅1 ‘ 𝑏 ) ) )
55 frsuc ⊢ ( 𝑏 ∈ ω → ( ( rec ( 𝐺 , ∅ ) ↾ ω ) ‘ suc 𝑏 ) = ( 𝐺 ‘ ( ( rec ( 𝐺 , ∅ ) ↾ ω ) ‘ 𝑏 ) ) )
56 peano2 ⊢ ( 𝑏 ∈ ω → suc 𝑏 ∈ ω )
57 56 fvresd ⊢ ( 𝑏 ∈ ω → ( ( rec ( 𝐺 , ∅ ) ↾ ω ) ‘ suc 𝑏 ) = ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) )
58 fvres ⊢ ( 𝑏 ∈ ω → ( ( rec ( 𝐺 , ∅ ) ↾ ω ) ‘ 𝑏 ) = ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) )
59 58 fveq2d ⊢ ( 𝑏 ∈ ω → ( 𝐺 ‘ ( ( rec ( 𝐺 , ∅ ) ↾ ω ) ‘ 𝑏 ) ) = ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ) )
60 fvex ⊢ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ∈ V
61 dmeq ⊢ ( 𝑥 = ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) → dom 𝑥 = dom ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) )
62 61 pweqd ⊢ ( 𝑥 = ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) → 𝒫 dom 𝑥 = 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) )
63 imaeq1 ⊢ ( 𝑥 = ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) → ( 𝑥 “ 𝑦 ) = ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑦 ) )
64 63 fveq2d ⊢ ( 𝑥 = ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) → ( 𝐹 ‘ ( 𝑥 “ 𝑦 ) ) = ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑦 ) ) )
65 62 64 mpteq12dv ⊢ ( 𝑥 = ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) → ( 𝑦 ∈ 𝒫 dom 𝑥 ↦ ( 𝐹 ‘ ( 𝑥 “ 𝑦 ) ) ) = ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑦 ) ) ) )
66 60 dmex ⊢ dom ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ∈ V
67 66 pwex ⊢ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ∈ V
68 67 mptex ⊢ ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑦 ) ) ) ∈ V
69 65 2 68 fvmpt ⊢ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ∈ V → ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ) = ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑦 ) ) ) )
70 60 69 ax-mp ⊢ ( 𝐺 ‘ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ) = ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑦 ) ) )
71 59 70 eqtrdi ⊢ ( 𝑏 ∈ ω → ( 𝐺 ‘ ( ( rec ( 𝐺 , ∅ ) ↾ ω ) ‘ 𝑏 ) ) = ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑦 ) ) ) )
72 55 57 71 3eqtr3d ⊢ ( 𝑏 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑦 ) ) ) )
73 72 adantr ⊢ ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) : ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑦 ) ) ) )
74 f1odm ⊢ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) : ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) → dom ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( 𝑅1 ‘ 𝑏 ) )
75 74 adantl ⊢ ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) : ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) → dom ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = ( 𝑅1 ‘ 𝑏 ) )
76 75 pweqd ⊢ ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) : ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) → 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) = 𝒫 ( 𝑅1 ‘ 𝑏 ) )
77 76 mpteq1d ⊢ ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) : ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) → ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑦 ) ) ) = ( 𝑦 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑦 ) ) ) )
78 fvex ⊢ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑦 ) ) ∈ V
79 eqid ⊢ ( 𝑦 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑦 ) ) ) = ( 𝑦 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑦 ) ) )
80 78 79 fnmpti ⊢ ( 𝑦 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑦 ) ) ) Fn 𝒫 ( 𝑅1 ‘ 𝑏 )
81 80 a1i ⊢ ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) : ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) → ( 𝑦 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑦 ) ) ) Fn 𝒫 ( 𝑅1 ‘ 𝑏 ) )
82 f1ofn ⊢ ( ( ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ∘ ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) ) : 𝒫 ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ 𝒫 ( 𝑅1 ‘ 𝑏 ) ) → ( ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ∘ ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) ) Fn 𝒫 ( 𝑅1 ‘ 𝑏 ) )
83 54 82 syl ⊢ ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) : ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) → ( ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ∘ ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) ) Fn 𝒫 ( 𝑅1 ‘ 𝑏 ) )
84 f1of ⊢ ( ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) : 𝒫 ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) → ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) : 𝒫 ( 𝑅1 ‘ 𝑏 ) ⟶ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) )
85 52 84 syl ⊢ ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) : ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) → ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) : 𝒫 ( 𝑅1 ‘ 𝑏 ) ⟶ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) )
86 85 ffvelrnda ⊢ ( ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) : ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ∧ 𝑐 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ) → ( ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) ‘ 𝑐 ) ∈ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) )
87 86 fvresd ⊢ ( ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) : ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ∧ 𝑐 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ) → ( ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ‘ ( ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) ‘ 𝑐 ) ) = ( 𝐹 ‘ ( ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) ‘ 𝑐 ) ) )
88 imaeq2 ⊢ ( 𝑎 = 𝑐 → ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) = ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑐 ) )
89 eqid ⊢ ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) = ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) )
90 60 imaex ⊢ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑐 ) ∈ V
91 88 89 90 fvmpt ⊢ ( 𝑐 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) → ( ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) ‘ 𝑐 ) = ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑐 ) )
92 91 adantl ⊢ ( ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) : ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ∧ 𝑐 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ) → ( ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) ‘ 𝑐 ) = ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑐 ) )
93 92 fveq2d ⊢ ( ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) : ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ∧ 𝑐 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ) → ( 𝐹 ‘ ( ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) ‘ 𝑐 ) ) = ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑐 ) ) )
94 87 93 eqtrd ⊢ ( ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) : ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ∧ 𝑐 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ) → ( ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ‘ ( ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) ‘ 𝑐 ) ) = ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑐 ) ) )
95 fvco3 ⊢ ( ( ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) : 𝒫 ( 𝑅1 ‘ 𝑏 ) ⟶ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ∧ 𝑐 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ) → ( ( ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ∘ ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) ) ‘ 𝑐 ) = ( ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ‘ ( ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) ‘ 𝑐 ) ) )
96 85 95 sylan ⊢ ( ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) : ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ∧ 𝑐 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ) → ( ( ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ∘ ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) ) ‘ 𝑐 ) = ( ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ‘ ( ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) ‘ 𝑐 ) ) )
97 imaeq2 ⊢ ( 𝑦 = 𝑐 → ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑦 ) = ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑐 ) )
98 97 fveq2d ⊢ ( 𝑦 = 𝑐 → ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑦 ) ) = ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑐 ) ) )
99 fvex ⊢ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑐 ) ) ∈ V
100 98 79 99 fvmpt ⊢ ( 𝑐 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) → ( ( 𝑦 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑦 ) ) ) ‘ 𝑐 ) = ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑐 ) ) )
101 100 adantl ⊢ ( ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) : ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ∧ 𝑐 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ) → ( ( 𝑦 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑦 ) ) ) ‘ 𝑐 ) = ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑐 ) ) )
102 94 96 101 3eqtr4rd ⊢ ( ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) : ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ∧ 𝑐 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ) → ( ( 𝑦 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑦 ) ) ) ‘ 𝑐 ) = ( ( ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ∘ ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) ) ‘ 𝑐 ) )
103 81 83 102 eqfnfvd ⊢ ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) : ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) → ( 𝑦 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑦 ) ) ) = ( ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ∘ ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) ) )
104 77 103 eqtrd ⊢ ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) : ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) → ( 𝑦 ∈ 𝒫 dom ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ↦ ( 𝐹 ‘ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑦 ) ) ) = ( ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ∘ ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) ) )
105 73 104 eqtrd ⊢ ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) : ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = ( ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ∘ ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) ) )
106 f1oeq1 ⊢ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = ( ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ∘ ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) ) → ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) : ( 𝑅1 ‘ suc 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) ↔ ( ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ∘ ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) ) : ( 𝑅1 ‘ suc 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) ) )
107 105 106 syl ⊢ ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) : ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) → ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) : ( 𝑅1 ‘ suc 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) ↔ ( ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ∘ ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) ) : ( 𝑅1 ‘ suc 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) ) )
108 nnon ⊢ ( 𝑏 ∈ ω → 𝑏 ∈ On )
109 r1suc ⊢ ( 𝑏 ∈ On → ( 𝑅1 ‘ suc 𝑏 ) = 𝒫 ( 𝑅1 ‘ 𝑏 ) )
110 108 109 syl ⊢ ( 𝑏 ∈ ω → ( 𝑅1 ‘ suc 𝑏 ) = 𝒫 ( 𝑅1 ‘ 𝑏 ) )
111 110 fveq2d ⊢ ( 𝑏 ∈ ω → ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) = ( card ‘ 𝒫 ( 𝑅1 ‘ 𝑏 ) ) )
112 f1oeq23 ⊢ ( ( ( 𝑅1 ‘ suc 𝑏 ) = 𝒫 ( 𝑅1 ‘ 𝑏 ) ∧ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) = ( card ‘ 𝒫 ( 𝑅1 ‘ 𝑏 ) ) ) → ( ( ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ∘ ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) ) : ( 𝑅1 ‘ suc 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) ↔ ( ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ∘ ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) ) : 𝒫 ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ 𝒫 ( 𝑅1 ‘ 𝑏 ) ) ) )
113 110 111 112 syl2anc ⊢ ( 𝑏 ∈ ω → ( ( ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ∘ ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) ) : ( 𝑅1 ‘ suc 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) ↔ ( ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ∘ ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) ) : 𝒫 ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ 𝒫 ( 𝑅1 ‘ 𝑏 ) ) ) )
114 113 adantr ⊢ ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) : ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) → ( ( ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ∘ ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) ) : ( 𝑅1 ‘ suc 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) ↔ ( ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ∘ ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) ) : 𝒫 ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ 𝒫 ( 𝑅1 ‘ 𝑏 ) ) ) )
115 107 114 bitrd ⊢ ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) : ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) → ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) : ( 𝑅1 ‘ suc 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) ↔ ( ( 𝐹 ↾ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) ∘ ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝑏 ) ↦ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) “ 𝑎 ) ) ) : 𝒫 ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ 𝒫 ( 𝑅1 ‘ 𝑏 ) ) ) )
116 54 115 mpbird ⊢ ( ( 𝑏 ∈ ω ∧ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) : ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) ) → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) : ( 𝑅1 ‘ suc 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) )
117 116 ex ⊢ ( 𝑏 ∈ ω → ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) : ( 𝑅1 ‘ 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑏 ) ) → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) : ( 𝑅1 ‘ suc 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) ) )
118 6 10 14 18 31 117 finds ⊢ ( 𝐴 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ 𝐴 ) : ( 𝑅1 ‘ 𝐴 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝐴 ) ) )