Metamath Proof Explorer

Theorem ackbij2

Description: The Ackermann bijection, part 2: hereditarily finite sets can be represented by recursive binary notation. (Contributed by Stefan O'Rear, 18-Nov-2014)

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

Proof

Step Hyp Ref Expression
1 ackbij.f ⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
2 ackbij.g ⊢ 𝐺 = ( 𝑥 ∈ V ↦ ( 𝑦 ∈ 𝒫 dom 𝑥 ↦ ( 𝐹 ‘ ( 𝑥 “ 𝑦 ) ) ) )
3 ackbij.h ⊢ 𝐻 = ∪ ( rec ( 𝐺 , ∅ ) “ ω )
4 fveq2 ⊢ ( 𝑎 = 𝑏 → ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) = ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) )
5 fvex ⊢ ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) ∈ V
6 4 5 f1iun ⊢ ( ∀ 𝑎 ∈ ω ( ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) : ( 𝑅1 ‘ 𝑎 ) –1-1→ ω ∧ ∀ 𝑏 ∈ ω ( ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ∨ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) ) ) → ∪ 𝑎 ∈ ω ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) : ∪ 𝑎 ∈ ω ( 𝑅1 ‘ 𝑎 ) –1-1→ ω )
7 1 2 ackbij2lem2 ⊢ ( 𝑎 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) : ( 𝑅1 ‘ 𝑎 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑎 ) ) )
8 f1of1 ⊢ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) : ( 𝑅1 ‘ 𝑎 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑎 ) ) → ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) : ( 𝑅1 ‘ 𝑎 ) –1-1→ ( card ‘ ( 𝑅1 ‘ 𝑎 ) ) )
9 7 8 syl ⊢ ( 𝑎 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) : ( 𝑅1 ‘ 𝑎 ) –1-1→ ( card ‘ ( 𝑅1 ‘ 𝑎 ) ) )
10 ordom ⊢ Ord ω
11 r1fin ⊢ ( 𝑎 ∈ ω → ( 𝑅1 ‘ 𝑎 ) ∈ Fin )
12 ficardom ⊢ ( ( 𝑅1 ‘ 𝑎 ) ∈ Fin → ( card ‘ ( 𝑅1 ‘ 𝑎 ) ) ∈ ω )
13 11 12 syl ⊢ ( 𝑎 ∈ ω → ( card ‘ ( 𝑅1 ‘ 𝑎 ) ) ∈ ω )
14 ordelss ⊢ ( ( Ord ω ∧ ( card ‘ ( 𝑅1 ‘ 𝑎 ) ) ∈ ω ) → ( card ‘ ( 𝑅1 ‘ 𝑎 ) ) ⊆ ω )
15 10 13 14 sylancr ⊢ ( 𝑎 ∈ ω → ( card ‘ ( 𝑅1 ‘ 𝑎 ) ) ⊆ ω )
16 f1ss ⊢ ( ( ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) : ( 𝑅1 ‘ 𝑎 ) –1-1→ ( card ‘ ( 𝑅1 ‘ 𝑎 ) ) ∧ ( card ‘ ( 𝑅1 ‘ 𝑎 ) ) ⊆ ω ) → ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) : ( 𝑅1 ‘ 𝑎 ) –1-1→ ω )
17 9 15 16 syl2anc ⊢ ( 𝑎 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) : ( 𝑅1 ‘ 𝑎 ) –1-1→ ω )
18 nnord ⊢ ( 𝑎 ∈ ω → Ord 𝑎 )
19 nnord ⊢ ( 𝑏 ∈ ω → Ord 𝑏 )
20 ordtri2or2 ⊢ ( ( Ord 𝑎 ∧ Ord 𝑏 ) → ( 𝑎 ⊆ 𝑏 ∨ 𝑏 ⊆ 𝑎 ) )
21 18 19 20 syl2an ⊢ ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( 𝑎 ⊆ 𝑏 ∨ 𝑏 ⊆ 𝑎 ) )
22 1 2 ackbij2lem4 ⊢ ( ( ( 𝑏 ∈ ω ∧ 𝑎 ∈ ω ) ∧ 𝑎 ⊆ 𝑏 ) → ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) )
23 22 ex ⊢ ( ( 𝑏 ∈ ω ∧ 𝑎 ∈ ω ) → ( 𝑎 ⊆ 𝑏 → ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ) )
24 23 ancoms ⊢ ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( 𝑎 ⊆ 𝑏 → ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ) )
25 1 2 ackbij2lem4 ⊢ ( ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ∧ 𝑏 ⊆ 𝑎 ) → ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) )
26 25 ex ⊢ ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( 𝑏 ⊆ 𝑎 → ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) ) )
27 24 26 orim12d ⊢ ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( ( 𝑎 ⊆ 𝑏 ∨ 𝑏 ⊆ 𝑎 ) → ( ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ∨ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) ) ) )
28 21 27 mpd ⊢ ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ∨ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) ) )
29 28 ralrimiva ⊢ ( 𝑎 ∈ ω → ∀ 𝑏 ∈ ω ( ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ∨ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) ) )
30 17 29 jca ⊢ ( 𝑎 ∈ ω → ( ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) : ( 𝑅1 ‘ 𝑎 ) –1-1→ ω ∧ ∀ 𝑏 ∈ ω ( ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ∨ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) ) ) )
31 6 30 mprg ⊢ ∪ 𝑎 ∈ ω ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) : ∪ 𝑎 ∈ ω ( 𝑅1 ‘ 𝑎 ) –1-1→ ω
32 rdgfun ⊢ Fun rec ( 𝐺 , ∅ )
33 funiunfv ⊢ ( Fun rec ( 𝐺 , ∅ ) → ∪ 𝑎 ∈ ω ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) = ∪ ( rec ( 𝐺 , ∅ ) “ ω ) )
34 33 eqcomd ⊢ ( Fun rec ( 𝐺 , ∅ ) → ∪ ( rec ( 𝐺 , ∅ ) “ ω ) = ∪ 𝑎 ∈ ω ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) )
35 f1eq1 ⊢ ( ∪ ( rec ( 𝐺 , ∅ ) “ ω ) = ∪ 𝑎 ∈ ω ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) → ( ∪ ( rec ( 𝐺 , ∅ ) “ ω ) : ∪ ( 𝑅1 “ ω ) –1-1→ ω ↔ ∪ 𝑎 ∈ ω ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) : ∪ ( 𝑅1 “ ω ) –1-1→ ω ) )
36 32 34 35 mp2b ⊢ ( ∪ ( rec ( 𝐺 , ∅ ) “ ω ) : ∪ ( 𝑅1 “ ω ) –1-1→ ω ↔ ∪ 𝑎 ∈ ω ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) : ∪ ( 𝑅1 “ ω ) –1-1→ ω )
37 r1funlim ⊢ ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
38 37 simpli ⊢ Fun 𝑅1
39 funiunfv ⊢ ( Fun 𝑅1 → ∪ 𝑎 ∈ ω ( 𝑅1 ‘ 𝑎 ) = ∪ ( 𝑅1 “ ω ) )
40 f1eq2 ⊢ ( ∪ 𝑎 ∈ ω ( 𝑅1 ‘ 𝑎 ) = ∪ ( 𝑅1 “ ω ) → ( ∪ 𝑎 ∈ ω ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) : ∪ 𝑎 ∈ ω ( 𝑅1 ‘ 𝑎 ) –1-1→ ω ↔ ∪ 𝑎 ∈ ω ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) : ∪ ( 𝑅1 “ ω ) –1-1→ ω ) )
41 38 39 40 mp2b ⊢ ( ∪ 𝑎 ∈ ω ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) : ∪ 𝑎 ∈ ω ( 𝑅1 ‘ 𝑎 ) –1-1→ ω ↔ ∪ 𝑎 ∈ ω ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) : ∪ ( 𝑅1 “ ω ) –1-1→ ω )
42 36 41 bitr4i ⊢ ( ∪ ( rec ( 𝐺 , ∅ ) “ ω ) : ∪ ( 𝑅1 “ ω ) –1-1→ ω ↔ ∪ 𝑎 ∈ ω ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) : ∪ 𝑎 ∈ ω ( 𝑅1 ‘ 𝑎 ) –1-1→ ω )
43 31 42 mpbir ⊢ ∪ ( rec ( 𝐺 , ∅ ) “ ω ) : ∪ ( 𝑅1 “ ω ) –1-1→ ω
44 rnuni ⊢ ran ∪ ( rec ( 𝐺 , ∅ ) “ ω ) = ∪ 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ran 𝑎
45 eliun ⊢ ( 𝑏 ∈ ∪ 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ran 𝑎 ↔ ∃ 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) 𝑏 ∈ ran 𝑎 )
46 df-rex ⊢ ( ∃ 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) 𝑏 ∈ ran 𝑎 ↔ ∃ 𝑎 ( 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ∧ 𝑏 ∈ ran 𝑎 ) )
47 funfn ⊢ ( Fun rec ( 𝐺 , ∅ ) ↔ rec ( 𝐺 , ∅ ) Fn dom rec ( 𝐺 , ∅ ) )
48 32 47 mpbi ⊢ rec ( 𝐺 , ∅ ) Fn dom rec ( 𝐺 , ∅ )
49 rdgdmlim ⊢ Lim dom rec ( 𝐺 , ∅ )
50 limomss ⊢ ( Lim dom rec ( 𝐺 , ∅ ) → ω ⊆ dom rec ( 𝐺 , ∅ ) )
51 49 50 ax-mp ⊢ ω ⊆ dom rec ( 𝐺 , ∅ )
52 fvelimab ⊢ ( ( rec ( 𝐺 , ∅ ) Fn dom rec ( 𝐺 , ∅ ) ∧ ω ⊆ dom rec ( 𝐺 , ∅ ) ) → ( 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ↔ ∃ 𝑐 ∈ ω ( rec ( 𝐺 , ∅ ) ‘ 𝑐 ) = 𝑎 ) )
53 48 51 52 mp2an ⊢ ( 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ↔ ∃ 𝑐 ∈ ω ( rec ( 𝐺 , ∅ ) ‘ 𝑐 ) = 𝑎 )
54 1 2 ackbij2lem2 ⊢ ( 𝑐 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ 𝑐 ) : ( 𝑅1 ‘ 𝑐 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑐 ) ) )
55 f1ofo ⊢ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑐 ) : ( 𝑅1 ‘ 𝑐 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑐 ) ) → ( rec ( 𝐺 , ∅ ) ‘ 𝑐 ) : ( 𝑅1 ‘ 𝑐 ) –onto→ ( card ‘ ( 𝑅1 ‘ 𝑐 ) ) )
56 forn ⊢ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑐 ) : ( 𝑅1 ‘ 𝑐 ) –onto→ ( card ‘ ( 𝑅1 ‘ 𝑐 ) ) → ran ( rec ( 𝐺 , ∅ ) ‘ 𝑐 ) = ( card ‘ ( 𝑅1 ‘ 𝑐 ) ) )
57 54 55 56 3syl ⊢ ( 𝑐 ∈ ω → ran ( rec ( 𝐺 , ∅ ) ‘ 𝑐 ) = ( card ‘ ( 𝑅1 ‘ 𝑐 ) ) )
58 r1fin ⊢ ( 𝑐 ∈ ω → ( 𝑅1 ‘ 𝑐 ) ∈ Fin )
59 ficardom ⊢ ( ( 𝑅1 ‘ 𝑐 ) ∈ Fin → ( card ‘ ( 𝑅1 ‘ 𝑐 ) ) ∈ ω )
60 58 59 syl ⊢ ( 𝑐 ∈ ω → ( card ‘ ( 𝑅1 ‘ 𝑐 ) ) ∈ ω )
61 ordelss ⊢ ( ( Ord ω ∧ ( card ‘ ( 𝑅1 ‘ 𝑐 ) ) ∈ ω ) → ( card ‘ ( 𝑅1 ‘ 𝑐 ) ) ⊆ ω )
62 10 60 61 sylancr ⊢ ( 𝑐 ∈ ω → ( card ‘ ( 𝑅1 ‘ 𝑐 ) ) ⊆ ω )
63 57 62 eqsstrd ⊢ ( 𝑐 ∈ ω → ran ( rec ( 𝐺 , ∅ ) ‘ 𝑐 ) ⊆ ω )
64 rneq ⊢ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑐 ) = 𝑎 → ran ( rec ( 𝐺 , ∅ ) ‘ 𝑐 ) = ran 𝑎 )
65 64 sseq1d ⊢ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑐 ) = 𝑎 → ( ran ( rec ( 𝐺 , ∅ ) ‘ 𝑐 ) ⊆ ω ↔ ran 𝑎 ⊆ ω ) )
66 63 65 syl5ibcom ⊢ ( 𝑐 ∈ ω → ( ( rec ( 𝐺 , ∅ ) ‘ 𝑐 ) = 𝑎 → ran 𝑎 ⊆ ω ) )
67 66 rexlimiv ⊢ ( ∃ 𝑐 ∈ ω ( rec ( 𝐺 , ∅ ) ‘ 𝑐 ) = 𝑎 → ran 𝑎 ⊆ ω )
68 53 67 sylbi ⊢ ( 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) → ran 𝑎 ⊆ ω )
69 68 sselda ⊢ ( ( 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ∧ 𝑏 ∈ ran 𝑎 ) → 𝑏 ∈ ω )
70 69 exlimiv ⊢ ( ∃ 𝑎 ( 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ∧ 𝑏 ∈ ran 𝑎 ) → 𝑏 ∈ ω )
71 peano2 ⊢ ( 𝑏 ∈ ω → suc 𝑏 ∈ ω )
72 fnfvima ⊢ ( ( rec ( 𝐺 , ∅ ) Fn dom rec ( 𝐺 , ∅ ) ∧ ω ⊆ dom rec ( 𝐺 , ∅ ) ∧ suc 𝑏 ∈ ω ) → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ∈ ( rec ( 𝐺 , ∅ ) “ ω ) )
73 48 51 71 72 mp3an12i ⊢ ( 𝑏 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ∈ ( rec ( 𝐺 , ∅ ) “ ω ) )
74 vex ⊢ 𝑏 ∈ V
75 cardnn ⊢ ( suc 𝑏 ∈ ω → ( card ‘ suc 𝑏 ) = suc 𝑏 )
76 fvex ⊢ ( 𝑅1 ‘ suc 𝑏 ) ∈ V
77 37 simpri ⊢ Lim dom 𝑅1
78 limomss ⊢ ( Lim dom 𝑅1 → ω ⊆ dom 𝑅1 )
79 77 78 ax-mp ⊢ ω ⊆ dom 𝑅1
80 79 sseli ⊢ ( suc 𝑏 ∈ ω → suc 𝑏 ∈ dom 𝑅1 )
81 onssr1 ⊢ ( suc 𝑏 ∈ dom 𝑅1 → suc 𝑏 ⊆ ( 𝑅1 ‘ suc 𝑏 ) )
82 80 81 syl ⊢ ( suc 𝑏 ∈ ω → suc 𝑏 ⊆ ( 𝑅1 ‘ suc 𝑏 ) )
83 ssdomg ⊢ ( ( 𝑅1 ‘ suc 𝑏 ) ∈ V → ( suc 𝑏 ⊆ ( 𝑅1 ‘ suc 𝑏 ) → suc 𝑏 ≼ ( 𝑅1 ‘ suc 𝑏 ) ) )
84 76 82 83 mpsyl ⊢ ( suc 𝑏 ∈ ω → suc 𝑏 ≼ ( 𝑅1 ‘ suc 𝑏 ) )
85 nnon ⊢ ( suc 𝑏 ∈ ω → suc 𝑏 ∈ On )
86 onenon ⊢ ( suc 𝑏 ∈ On → suc 𝑏 ∈ dom card )
87 85 86 syl ⊢ ( suc 𝑏 ∈ ω → suc 𝑏 ∈ dom card )
88 r1fin ⊢ ( suc 𝑏 ∈ ω → ( 𝑅1 ‘ suc 𝑏 ) ∈ Fin )
89 finnum ⊢ ( ( 𝑅1 ‘ suc 𝑏 ) ∈ Fin → ( 𝑅1 ‘ suc 𝑏 ) ∈ dom card )
90 88 89 syl ⊢ ( suc 𝑏 ∈ ω → ( 𝑅1 ‘ suc 𝑏 ) ∈ dom card )
91 carddom2 ⊢ ( ( suc 𝑏 ∈ dom card ∧ ( 𝑅1 ‘ suc 𝑏 ) ∈ dom card ) → ( ( card ‘ suc 𝑏 ) ⊆ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) ↔ suc 𝑏 ≼ ( 𝑅1 ‘ suc 𝑏 ) ) )
92 87 90 91 syl2anc ⊢ ( suc 𝑏 ∈ ω → ( ( card ‘ suc 𝑏 ) ⊆ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) ↔ suc 𝑏 ≼ ( 𝑅1 ‘ suc 𝑏 ) ) )
93 84 92 mpbird ⊢ ( suc 𝑏 ∈ ω → ( card ‘ suc 𝑏 ) ⊆ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) )
94 75 93 eqsstrrd ⊢ ( suc 𝑏 ∈ ω → suc 𝑏 ⊆ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) )
95 71 94 syl ⊢ ( 𝑏 ∈ ω → suc 𝑏 ⊆ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) )
96 sucssel ⊢ ( 𝑏 ∈ V → ( suc 𝑏 ⊆ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) → 𝑏 ∈ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) ) )
97 74 95 96 mpsyl ⊢ ( 𝑏 ∈ ω → 𝑏 ∈ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) )
98 1 2 ackbij2lem2 ⊢ ( suc 𝑏 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) : ( 𝑅1 ‘ suc 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) )
99 f1ofo ⊢ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) : ( 𝑅1 ‘ suc 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) : ( 𝑅1 ‘ suc 𝑏 ) –onto→ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) )
100 forn ⊢ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) : ( 𝑅1 ‘ suc 𝑏 ) –onto→ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) → ran ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) )
101 71 98 99 100 4syl ⊢ ( 𝑏 ∈ ω → ran ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) )
102 97 101 eleqtrrd ⊢ ( 𝑏 ∈ ω → 𝑏 ∈ ran ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) )
103 fvex ⊢ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ∈ V
104 eleq1 ⊢ ( 𝑎 = ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) → ( 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ↔ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ) )
105 rneq ⊢ ( 𝑎 = ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) → ran 𝑎 = ran ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) )
106 105 eleq2d ⊢ ( 𝑎 = ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) → ( 𝑏 ∈ ran 𝑎 ↔ 𝑏 ∈ ran ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) )
107 104 106 anbi12d ⊢ ( 𝑎 = ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) → ( ( 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ∧ 𝑏 ∈ ran 𝑎 ) ↔ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ∧ 𝑏 ∈ ran ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) ) )
108 103 107 spcev ⊢ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ∧ 𝑏 ∈ ran ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) → ∃ 𝑎 ( 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ∧ 𝑏 ∈ ran 𝑎 ) )
109 73 102 108 syl2anc ⊢ ( 𝑏 ∈ ω → ∃ 𝑎 ( 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ∧ 𝑏 ∈ ran 𝑎 ) )
110 70 109 impbii ⊢ ( ∃ 𝑎 ( 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ∧ 𝑏 ∈ ran 𝑎 ) ↔ 𝑏 ∈ ω )
111 45 46 110 3bitri ⊢ ( 𝑏 ∈ ∪ 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ran 𝑎 ↔ 𝑏 ∈ ω )
112 111 eqriv ⊢ ∪ 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ran 𝑎 = ω
113 44 112 eqtri ⊢ ran ∪ ( rec ( 𝐺 , ∅ ) “ ω ) = ω
114 dff1o5 ⊢ ( ∪ ( rec ( 𝐺 , ∅ ) “ ω ) : ∪ ( 𝑅1 “ ω ) –1-1-onto→ ω ↔ ( ∪ ( rec ( 𝐺 , ∅ ) “ ω ) : ∪ ( 𝑅1 “ ω ) –1-1→ ω ∧ ran ∪ ( rec ( 𝐺 , ∅ ) “ ω ) = ω ) )
115 43 113 114 mpbir2an ⊢ ∪ ( rec ( 𝐺 , ∅ ) “ ω ) : ∪ ( 𝑅1 “ ω ) –1-1-onto→ ω
116 f1oeq1 ⊢ ( 𝐻 = ∪ ( rec ( 𝐺 , ∅ ) “ ω ) → ( 𝐻 : ∪ ( 𝑅1 “ ω ) –1-1-onto→ ω ↔ ∪ ( rec ( 𝐺 , ∅ ) “ ω ) : ∪ ( 𝑅1 “ ω ) –1-1-onto→ ω ) )
117 3 116 ax-mp ⊢ ( 𝐻 : ∪ ( 𝑅1 “ ω ) –1-1-onto→ ω ↔ ∪ ( rec ( 𝐺 , ∅ ) “ ω ) : ∪ ( 𝑅1 “ ω ) –1-1-onto→ ω )
118 115 117 mpbir ⊢ 𝐻 : ∪ ( 𝑅1 “ ω ) –1-1-onto→ ω