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) Restate using the defined HF symbol. (Revised by Eric Schmidt, 24-Sep-2026)

Ref Expression
Hypotheses ackbij.f ⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
ackbij.g ⊢ 𝐺 = ( 𝑥 ∈ V ↦ ( 𝑦 ∈ 𝒫 dom 𝑥 ↦ ( 𝐹 ‘ ( 𝑥 “ 𝑦 ) ) ) )
ackbij.h ⊢ 𝐻 = ∪ ( rec ( 𝐺 , ∅ ) “ ω )
Assertion ackbij2 𝐻 : HF –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 ( 𝐺 , ∅ ) “ ω ) : HF –1-1→ ω ↔ ∪ 𝑎 ∈ ω ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) : HF –1-1→ ω ) )
36 32 34 35 mp2b ⊢ ( ∪ ( rec ( 𝐺 , ∅ ) “ ω ) : HF –1-1→ ω ↔ ∪ 𝑎 ∈ ω ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) : HF –1-1→ ω )
37 r1fun ⊢ Fun 𝑅1
38 funiunfv ⊢ ( Fun 𝑅1 → ∪ 𝑎 ∈ ω ( 𝑅1 ‘ 𝑎 ) = ∪ ( 𝑅1 “ ω ) )
39 df-hf ⊢ HF = ∪ ( 𝑅1 “ ω )
40 38 39 eqtr4di ⊢ ( Fun 𝑅1 → ∪ 𝑎 ∈ ω ( 𝑅1 ‘ 𝑎 ) = HF )
41 f1eq2 ⊢ ( ∪ 𝑎 ∈ ω ( 𝑅1 ‘ 𝑎 ) = HF → ( ∪ 𝑎 ∈ ω ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) : ∪ 𝑎 ∈ ω ( 𝑅1 ‘ 𝑎 ) –1-1→ ω ↔ ∪ 𝑎 ∈ ω ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) : HF –1-1→ ω ) )
42 37 40 41 mp2b ⊢ ( ∪ 𝑎 ∈ ω ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) : ∪ 𝑎 ∈ ω ( 𝑅1 ‘ 𝑎 ) –1-1→ ω ↔ ∪ 𝑎 ∈ ω ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) : HF –1-1→ ω )
43 36 42 bitr4i ⊢ ( ∪ ( rec ( 𝐺 , ∅ ) “ ω ) : HF –1-1→ ω ↔ ∪ 𝑎 ∈ ω ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) : ∪ 𝑎 ∈ ω ( 𝑅1 ‘ 𝑎 ) –1-1→ ω )
44 31 43 mpbir ⊢ ∪ ( rec ( 𝐺 , ∅ ) “ ω ) : HF –1-1→ ω
45 rnuni ⊢ ran ∪ ( rec ( 𝐺 , ∅ ) “ ω ) = ∪ 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ran 𝑎
46 eliun ⊢ ( 𝑏 ∈ ∪ 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ran 𝑎 ↔ ∃ 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) 𝑏 ∈ ran 𝑎 )
47 df-rex ⊢ ( ∃ 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) 𝑏 ∈ ran 𝑎 ↔ ∃ 𝑎 ( 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ∧ 𝑏 ∈ ran 𝑎 ) )
48 funfn ⊢ ( Fun rec ( 𝐺 , ∅ ) ↔ rec ( 𝐺 , ∅ ) Fn dom rec ( 𝐺 , ∅ ) )
49 32 48 mpbi ⊢ rec ( 𝐺 , ∅ ) Fn dom rec ( 𝐺 , ∅ )
50 rdgdmlim ⊢ Lim dom rec ( 𝐺 , ∅ )
51 limomss ⊢ ( Lim dom rec ( 𝐺 , ∅ ) → ω ⊆ dom rec ( 𝐺 , ∅ ) )
52 50 51 ax-mp ⊢ ω ⊆ dom rec ( 𝐺 , ∅ )
53 fvelimab ⊢ ( ( rec ( 𝐺 , ∅ ) Fn dom rec ( 𝐺 , ∅ ) ∧ ω ⊆ dom rec ( 𝐺 , ∅ ) ) → ( 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ↔ ∃ 𝑐 ∈ ω ( rec ( 𝐺 , ∅ ) ‘ 𝑐 ) = 𝑎 ) )
54 49 52 53 mp2an ⊢ ( 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ↔ ∃ 𝑐 ∈ ω ( rec ( 𝐺 , ∅ ) ‘ 𝑐 ) = 𝑎 )
55 1 2 ackbij2lem2 ⊢ ( 𝑐 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ 𝑐 ) : ( 𝑅1 ‘ 𝑐 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑐 ) ) )
56 f1ofo ⊢ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑐 ) : ( 𝑅1 ‘ 𝑐 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ 𝑐 ) ) → ( rec ( 𝐺 , ∅ ) ‘ 𝑐 ) : ( 𝑅1 ‘ 𝑐 ) –onto→ ( card ‘ ( 𝑅1 ‘ 𝑐 ) ) )
57 forn ⊢ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑐 ) : ( 𝑅1 ‘ 𝑐 ) –onto→ ( card ‘ ( 𝑅1 ‘ 𝑐 ) ) → ran ( rec ( 𝐺 , ∅ ) ‘ 𝑐 ) = ( card ‘ ( 𝑅1 ‘ 𝑐 ) ) )
58 55 56 57 3syl ⊢ ( 𝑐 ∈ ω → ran ( rec ( 𝐺 , ∅ ) ‘ 𝑐 ) = ( card ‘ ( 𝑅1 ‘ 𝑐 ) ) )
59 r1fin ⊢ ( 𝑐 ∈ ω → ( 𝑅1 ‘ 𝑐 ) ∈ Fin )
60 ficardom ⊢ ( ( 𝑅1 ‘ 𝑐 ) ∈ Fin → ( card ‘ ( 𝑅1 ‘ 𝑐 ) ) ∈ ω )
61 59 60 syl ⊢ ( 𝑐 ∈ ω → ( card ‘ ( 𝑅1 ‘ 𝑐 ) ) ∈ ω )
62 ordelss ⊢ ( ( Ord ω ∧ ( card ‘ ( 𝑅1 ‘ 𝑐 ) ) ∈ ω ) → ( card ‘ ( 𝑅1 ‘ 𝑐 ) ) ⊆ ω )
63 10 61 62 sylancr ⊢ ( 𝑐 ∈ ω → ( card ‘ ( 𝑅1 ‘ 𝑐 ) ) ⊆ ω )
64 58 63 eqsstrd ⊢ ( 𝑐 ∈ ω → ran ( rec ( 𝐺 , ∅ ) ‘ 𝑐 ) ⊆ ω )
65 rneq ⊢ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑐 ) = 𝑎 → ran ( rec ( 𝐺 , ∅ ) ‘ 𝑐 ) = ran 𝑎 )
66 65 sseq1d ⊢ ( ( rec ( 𝐺 , ∅ ) ‘ 𝑐 ) = 𝑎 → ( ran ( rec ( 𝐺 , ∅ ) ‘ 𝑐 ) ⊆ ω ↔ ran 𝑎 ⊆ ω ) )
67 64 66 syl5ibcom ⊢ ( 𝑐 ∈ ω → ( ( rec ( 𝐺 , ∅ ) ‘ 𝑐 ) = 𝑎 → ran 𝑎 ⊆ ω ) )
68 67 rexlimiv ⊢ ( ∃ 𝑐 ∈ ω ( rec ( 𝐺 , ∅ ) ‘ 𝑐 ) = 𝑎 → ran 𝑎 ⊆ ω )
69 54 68 sylbi ⊢ ( 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) → ran 𝑎 ⊆ ω )
70 69 sselda ⊢ ( ( 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ∧ 𝑏 ∈ ran 𝑎 ) → 𝑏 ∈ ω )
71 70 exlimiv ⊢ ( ∃ 𝑎 ( 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ∧ 𝑏 ∈ ran 𝑎 ) → 𝑏 ∈ ω )
72 peano2 ⊢ ( 𝑏 ∈ ω → suc 𝑏 ∈ ω )
73 fnfvima ⊢ ( ( rec ( 𝐺 , ∅ ) Fn dom rec ( 𝐺 , ∅ ) ∧ ω ⊆ dom rec ( 𝐺 , ∅ ) ∧ suc 𝑏 ∈ ω ) → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ∈ ( rec ( 𝐺 , ∅ ) “ ω ) )
74 49 52 72 73 mp3an12i ⊢ ( 𝑏 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ∈ ( rec ( 𝐺 , ∅ ) “ ω ) )
75 vex ⊢ 𝑏 ∈ V
76 cardnn ⊢ ( suc 𝑏 ∈ ω → ( card ‘ suc 𝑏 ) = suc 𝑏 )
77 fvex ⊢ ( 𝑅1 ‘ suc 𝑏 ) ∈ V
78 r1dmlim ⊢ Lim dom 𝑅1
79 limomss ⊢ ( Lim dom 𝑅1 → ω ⊆ dom 𝑅1 )
80 78 79 ax-mp ⊢ ω ⊆ dom 𝑅1
81 80 sseli ⊢ ( suc 𝑏 ∈ ω → suc 𝑏 ∈ dom 𝑅1 )
82 onssr1 ⊢ ( suc 𝑏 ∈ dom 𝑅1 → suc 𝑏 ⊆ ( 𝑅1 ‘ suc 𝑏 ) )
83 81 82 syl ⊢ ( suc 𝑏 ∈ ω → suc 𝑏 ⊆ ( 𝑅1 ‘ suc 𝑏 ) )
84 ssdomg ⊢ ( ( 𝑅1 ‘ suc 𝑏 ) ∈ V → ( suc 𝑏 ⊆ ( 𝑅1 ‘ suc 𝑏 ) → suc 𝑏 ≼ ( 𝑅1 ‘ suc 𝑏 ) ) )
85 77 83 84 mpsyl ⊢ ( suc 𝑏 ∈ ω → suc 𝑏 ≼ ( 𝑅1 ‘ suc 𝑏 ) )
86 nnon ⊢ ( suc 𝑏 ∈ ω → suc 𝑏 ∈ On )
87 onenon ⊢ ( suc 𝑏 ∈ On → suc 𝑏 ∈ dom card )
88 86 87 syl ⊢ ( suc 𝑏 ∈ ω → suc 𝑏 ∈ dom card )
89 r1fin ⊢ ( suc 𝑏 ∈ ω → ( 𝑅1 ‘ suc 𝑏 ) ∈ Fin )
90 finnum ⊢ ( ( 𝑅1 ‘ suc 𝑏 ) ∈ Fin → ( 𝑅1 ‘ suc 𝑏 ) ∈ dom card )
91 89 90 syl ⊢ ( suc 𝑏 ∈ ω → ( 𝑅1 ‘ suc 𝑏 ) ∈ dom card )
92 carddom2 ⊢ ( ( suc 𝑏 ∈ dom card ∧ ( 𝑅1 ‘ suc 𝑏 ) ∈ dom card ) → ( ( card ‘ suc 𝑏 ) ⊆ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) ↔ suc 𝑏 ≼ ( 𝑅1 ‘ suc 𝑏 ) ) )
93 88 91 92 syl2anc ⊢ ( suc 𝑏 ∈ ω → ( ( card ‘ suc 𝑏 ) ⊆ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) ↔ suc 𝑏 ≼ ( 𝑅1 ‘ suc 𝑏 ) ) )
94 85 93 mpbird ⊢ ( suc 𝑏 ∈ ω → ( card ‘ suc 𝑏 ) ⊆ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) )
95 76 94 eqsstrrd ⊢ ( suc 𝑏 ∈ ω → suc 𝑏 ⊆ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) )
96 72 95 syl ⊢ ( 𝑏 ∈ ω → suc 𝑏 ⊆ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) )
97 sucssel ⊢ ( 𝑏 ∈ V → ( suc 𝑏 ⊆ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) → 𝑏 ∈ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) ) )
98 75 96 97 mpsyl ⊢ ( 𝑏 ∈ ω → 𝑏 ∈ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) )
99 1 2 ackbij2lem2 ⊢ ( suc 𝑏 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) : ( 𝑅1 ‘ suc 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) )
100 f1ofo ⊢ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) : ( 𝑅1 ‘ suc 𝑏 ) –1-1-onto→ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) → ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) : ( 𝑅1 ‘ suc 𝑏 ) –onto→ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) )
101 forn ⊢ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) : ( 𝑅1 ‘ suc 𝑏 ) –onto→ ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) → ran ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) )
102 72 99 100 101 4syl ⊢ ( 𝑏 ∈ ω → ran ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) = ( card ‘ ( 𝑅1 ‘ suc 𝑏 ) ) )
103 98 102 eleqtrrd ⊢ ( 𝑏 ∈ ω → 𝑏 ∈ ran ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) )
104 fvex ⊢ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ∈ V
105 eleq1 ⊢ ( 𝑎 = ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) → ( 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ↔ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ) )
106 rneq ⊢ ( 𝑎 = ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) → ran 𝑎 = ran ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) )
107 106 eleq2d ⊢ ( 𝑎 = ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) → ( 𝑏 ∈ ran 𝑎 ↔ 𝑏 ∈ ran ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) )
108 105 107 anbi12d ⊢ ( 𝑎 = ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) → ( ( 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ∧ 𝑏 ∈ ran 𝑎 ) ↔ ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ∧ 𝑏 ∈ ran ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) ) )
109 104 108 spcev ⊢ ( ( ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ∧ 𝑏 ∈ ran ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) → ∃ 𝑎 ( 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ∧ 𝑏 ∈ ran 𝑎 ) )
110 74 103 109 syl2anc ⊢ ( 𝑏 ∈ ω → ∃ 𝑎 ( 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ∧ 𝑏 ∈ ran 𝑎 ) )
111 71 110 impbii ⊢ ( ∃ 𝑎 ( 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ∧ 𝑏 ∈ ran 𝑎 ) ↔ 𝑏 ∈ ω )
112 46 47 111 3bitri ⊢ ( 𝑏 ∈ ∪ 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ran 𝑎 ↔ 𝑏 ∈ ω )
113 112 eqriv ⊢ ∪ 𝑎 ∈ ( rec ( 𝐺 , ∅ ) “ ω ) ran 𝑎 = ω
114 45 113 eqtri ⊢ ran ∪ ( rec ( 𝐺 , ∅ ) “ ω ) = ω
115 dff1o5 ⊢ ( ∪ ( rec ( 𝐺 , ∅ ) “ ω ) : HF –1-1-onto→ ω ↔ ( ∪ ( rec ( 𝐺 , ∅ ) “ ω ) : HF –1-1→ ω ∧ ran ∪ ( rec ( 𝐺 , ∅ ) “ ω ) = ω ) )
116 44 114 115 mpbir2an ⊢ ∪ ( rec ( 𝐺 , ∅ ) “ ω ) : HF –1-1-onto→ ω
117 f1oeq1 ⊢ ( 𝐻 = ∪ ( rec ( 𝐺 , ∅ ) “ ω ) → ( 𝐻 : HF –1-1-onto→ ω ↔ ∪ ( rec ( 𝐺 , ∅ ) “ ω ) : HF –1-1-onto→ ω ) )
118 3 117 ax-mp ⊢ ( 𝐻 : HF –1-1-onto→ ω ↔ ∪ ( rec ( 𝐺 , ∅ ) “ ω ) : HF –1-1-onto→ ω )
119 116 118 mpbir ⊢ 𝐻 : HF –1-1-onto→ ω