# 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 ${⊢}{F}=\left({x}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{{y}\in {x}}\left(\left\{{y}\right\}×𝒫{y}\right)\right)\right)$
ackbij.g ${⊢}{G}=\left({x}\in \mathrm{V}⟼\left({y}\in 𝒫\mathrm{dom}{x}⟼{F}\left({x}\left[{y}\right]\right)\right)\right)$
ackbij.h ${⊢}{H}=\bigcup \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]$
Assertion ackbij2 ${⊢}{H}:\bigcup {R}_{1}\left[\mathrm{\omega }\right]\underset{1-1 onto}{⟶}\mathrm{\omega }$

### Proof

Step Hyp Ref Expression
1 ackbij.f ${⊢}{F}=\left({x}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{{y}\in {x}}\left(\left\{{y}\right\}×𝒫{y}\right)\right)\right)$
2 ackbij.g ${⊢}{G}=\left({x}\in \mathrm{V}⟼\left({y}\in 𝒫\mathrm{dom}{x}⟼{F}\left({x}\left[{y}\right]\right)\right)\right)$
3 ackbij.h ${⊢}{H}=\bigcup \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]$
4 fveq2 ${⊢}{a}={b}\to \mathrm{rec}\left({G},\varnothing \right)\left({a}\right)=\mathrm{rec}\left({G},\varnothing \right)\left({b}\right)$
5 fvex ${⊢}\mathrm{rec}\left({G},\varnothing \right)\left({a}\right)\in \mathrm{V}$
6 4 5 f1iun ${⊢}\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{rec}\left({G},\varnothing \right)\left({a}\right):{R}_{1}\left({a}\right)\underset{1-1}{⟶}\mathrm{\omega }\wedge \forall {b}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{rec}\left({G},\varnothing \right)\left({a}\right)\subseteq \mathrm{rec}\left({G},\varnothing \right)\left({b}\right)\vee \mathrm{rec}\left({G},\varnothing \right)\left({b}\right)\subseteq \mathrm{rec}\left({G},\varnothing \right)\left({a}\right)\right)\right)\to \bigcup _{{a}\in \mathrm{\omega }}\mathrm{rec}\left({G},\varnothing \right)\left({a}\right):\bigcup _{{a}\in \mathrm{\omega }}{R}_{1}\left({a}\right)\underset{1-1}{⟶}\mathrm{\omega }$
7 1 2 ackbij2lem2 ${⊢}{a}\in \mathrm{\omega }\to \mathrm{rec}\left({G},\varnothing \right)\left({a}\right):{R}_{1}\left({a}\right)\underset{1-1 onto}{⟶}\mathrm{card}\left({R}_{1}\left({a}\right)\right)$
8 f1of1 ${⊢}\mathrm{rec}\left({G},\varnothing \right)\left({a}\right):{R}_{1}\left({a}\right)\underset{1-1 onto}{⟶}\mathrm{card}\left({R}_{1}\left({a}\right)\right)\to \mathrm{rec}\left({G},\varnothing \right)\left({a}\right):{R}_{1}\left({a}\right)\underset{1-1}{⟶}\mathrm{card}\left({R}_{1}\left({a}\right)\right)$
9 7 8 syl ${⊢}{a}\in \mathrm{\omega }\to \mathrm{rec}\left({G},\varnothing \right)\left({a}\right):{R}_{1}\left({a}\right)\underset{1-1}{⟶}\mathrm{card}\left({R}_{1}\left({a}\right)\right)$
10 ordom ${⊢}\mathrm{Ord}\mathrm{\omega }$
11 r1fin ${⊢}{a}\in \mathrm{\omega }\to {R}_{1}\left({a}\right)\in \mathrm{Fin}$
12 ficardom ${⊢}{R}_{1}\left({a}\right)\in \mathrm{Fin}\to \mathrm{card}\left({R}_{1}\left({a}\right)\right)\in \mathrm{\omega }$
13 11 12 syl ${⊢}{a}\in \mathrm{\omega }\to \mathrm{card}\left({R}_{1}\left({a}\right)\right)\in \mathrm{\omega }$
14 ordelss ${⊢}\left(\mathrm{Ord}\mathrm{\omega }\wedge \mathrm{card}\left({R}_{1}\left({a}\right)\right)\in \mathrm{\omega }\right)\to \mathrm{card}\left({R}_{1}\left({a}\right)\right)\subseteq \mathrm{\omega }$
15 10 13 14 sylancr ${⊢}{a}\in \mathrm{\omega }\to \mathrm{card}\left({R}_{1}\left({a}\right)\right)\subseteq \mathrm{\omega }$
16 f1ss ${⊢}\left(\mathrm{rec}\left({G},\varnothing \right)\left({a}\right):{R}_{1}\left({a}\right)\underset{1-1}{⟶}\mathrm{card}\left({R}_{1}\left({a}\right)\right)\wedge \mathrm{card}\left({R}_{1}\left({a}\right)\right)\subseteq \mathrm{\omega }\right)\to \mathrm{rec}\left({G},\varnothing \right)\left({a}\right):{R}_{1}\left({a}\right)\underset{1-1}{⟶}\mathrm{\omega }$
17 9 15 16 syl2anc ${⊢}{a}\in \mathrm{\omega }\to \mathrm{rec}\left({G},\varnothing \right)\left({a}\right):{R}_{1}\left({a}\right)\underset{1-1}{⟶}\mathrm{\omega }$
18 nnord ${⊢}{a}\in \mathrm{\omega }\to \mathrm{Ord}{a}$
19 nnord ${⊢}{b}\in \mathrm{\omega }\to \mathrm{Ord}{b}$
20 ordtri2or2 ${⊢}\left(\mathrm{Ord}{a}\wedge \mathrm{Ord}{b}\right)\to \left({a}\subseteq {b}\vee {b}\subseteq {a}\right)$
21 18 19 20 syl2an ${⊢}\left({a}\in \mathrm{\omega }\wedge {b}\in \mathrm{\omega }\right)\to \left({a}\subseteq {b}\vee {b}\subseteq {a}\right)$
22 1 2 ackbij2lem4 ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge {a}\in \mathrm{\omega }\right)\wedge {a}\subseteq {b}\right)\to \mathrm{rec}\left({G},\varnothing \right)\left({a}\right)\subseteq \mathrm{rec}\left({G},\varnothing \right)\left({b}\right)$
23 22 ex ${⊢}\left({b}\in \mathrm{\omega }\wedge {a}\in \mathrm{\omega }\right)\to \left({a}\subseteq {b}\to \mathrm{rec}\left({G},\varnothing \right)\left({a}\right)\subseteq \mathrm{rec}\left({G},\varnothing \right)\left({b}\right)\right)$
24 23 ancoms ${⊢}\left({a}\in \mathrm{\omega }\wedge {b}\in \mathrm{\omega }\right)\to \left({a}\subseteq {b}\to \mathrm{rec}\left({G},\varnothing \right)\left({a}\right)\subseteq \mathrm{rec}\left({G},\varnothing \right)\left({b}\right)\right)$
25 1 2 ackbij2lem4 ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge {b}\in \mathrm{\omega }\right)\wedge {b}\subseteq {a}\right)\to \mathrm{rec}\left({G},\varnothing \right)\left({b}\right)\subseteq \mathrm{rec}\left({G},\varnothing \right)\left({a}\right)$
26 25 ex ${⊢}\left({a}\in \mathrm{\omega }\wedge {b}\in \mathrm{\omega }\right)\to \left({b}\subseteq {a}\to \mathrm{rec}\left({G},\varnothing \right)\left({b}\right)\subseteq \mathrm{rec}\left({G},\varnothing \right)\left({a}\right)\right)$
27 24 26 orim12d ${⊢}\left({a}\in \mathrm{\omega }\wedge {b}\in \mathrm{\omega }\right)\to \left(\left({a}\subseteq {b}\vee {b}\subseteq {a}\right)\to \left(\mathrm{rec}\left({G},\varnothing \right)\left({a}\right)\subseteq \mathrm{rec}\left({G},\varnothing \right)\left({b}\right)\vee \mathrm{rec}\left({G},\varnothing \right)\left({b}\right)\subseteq \mathrm{rec}\left({G},\varnothing \right)\left({a}\right)\right)\right)$
28 21 27 mpd ${⊢}\left({a}\in \mathrm{\omega }\wedge {b}\in \mathrm{\omega }\right)\to \left(\mathrm{rec}\left({G},\varnothing \right)\left({a}\right)\subseteq \mathrm{rec}\left({G},\varnothing \right)\left({b}\right)\vee \mathrm{rec}\left({G},\varnothing \right)\left({b}\right)\subseteq \mathrm{rec}\left({G},\varnothing \right)\left({a}\right)\right)$
29 28 ralrimiva ${⊢}{a}\in \mathrm{\omega }\to \forall {b}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{rec}\left({G},\varnothing \right)\left({a}\right)\subseteq \mathrm{rec}\left({G},\varnothing \right)\left({b}\right)\vee \mathrm{rec}\left({G},\varnothing \right)\left({b}\right)\subseteq \mathrm{rec}\left({G},\varnothing \right)\left({a}\right)\right)$
30 17 29 jca ${⊢}{a}\in \mathrm{\omega }\to \left(\mathrm{rec}\left({G},\varnothing \right)\left({a}\right):{R}_{1}\left({a}\right)\underset{1-1}{⟶}\mathrm{\omega }\wedge \forall {b}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(\mathrm{rec}\left({G},\varnothing \right)\left({a}\right)\subseteq \mathrm{rec}\left({G},\varnothing \right)\left({b}\right)\vee \mathrm{rec}\left({G},\varnothing \right)\left({b}\right)\subseteq \mathrm{rec}\left({G},\varnothing \right)\left({a}\right)\right)\right)$
31 6 30 mprg ${⊢}\bigcup _{{a}\in \mathrm{\omega }}\mathrm{rec}\left({G},\varnothing \right)\left({a}\right):\bigcup _{{a}\in \mathrm{\omega }}{R}_{1}\left({a}\right)\underset{1-1}{⟶}\mathrm{\omega }$
32 rdgfun ${⊢}\mathrm{Fun}\mathrm{rec}\left({G},\varnothing \right)$
33 funiunfv ${⊢}\mathrm{Fun}\mathrm{rec}\left({G},\varnothing \right)\to \bigcup _{{a}\in \mathrm{\omega }}\mathrm{rec}\left({G},\varnothing \right)\left({a}\right)=\bigcup \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]$
34 33 eqcomd ${⊢}\mathrm{Fun}\mathrm{rec}\left({G},\varnothing \right)\to \bigcup \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]=\bigcup _{{a}\in \mathrm{\omega }}\mathrm{rec}\left({G},\varnothing \right)\left({a}\right)$
35 f1eq1 ${⊢}\bigcup \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]=\bigcup _{{a}\in \mathrm{\omega }}\mathrm{rec}\left({G},\varnothing \right)\left({a}\right)\to \left(\bigcup \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]:\bigcup {R}_{1}\left[\mathrm{\omega }\right]\underset{1-1}{⟶}\mathrm{\omega }↔\bigcup _{{a}\in \mathrm{\omega }}\mathrm{rec}\left({G},\varnothing \right)\left({a}\right):\bigcup {R}_{1}\left[\mathrm{\omega }\right]\underset{1-1}{⟶}\mathrm{\omega }\right)$
36 32 34 35 mp2b ${⊢}\bigcup \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]:\bigcup {R}_{1}\left[\mathrm{\omega }\right]\underset{1-1}{⟶}\mathrm{\omega }↔\bigcup _{{a}\in \mathrm{\omega }}\mathrm{rec}\left({G},\varnothing \right)\left({a}\right):\bigcup {R}_{1}\left[\mathrm{\omega }\right]\underset{1-1}{⟶}\mathrm{\omega }$
37 r1funlim ${⊢}\left(\mathrm{Fun}{R}_{1}\wedge \mathrm{Lim}\mathrm{dom}{R}_{1}\right)$
38 37 simpli ${⊢}\mathrm{Fun}{R}_{1}$
39 funiunfv ${⊢}\mathrm{Fun}{R}_{1}\to \bigcup _{{a}\in \mathrm{\omega }}{R}_{1}\left({a}\right)=\bigcup {R}_{1}\left[\mathrm{\omega }\right]$
40 f1eq2 ${⊢}\bigcup _{{a}\in \mathrm{\omega }}{R}_{1}\left({a}\right)=\bigcup {R}_{1}\left[\mathrm{\omega }\right]\to \left(\bigcup _{{a}\in \mathrm{\omega }}\mathrm{rec}\left({G},\varnothing \right)\left({a}\right):\bigcup _{{a}\in \mathrm{\omega }}{R}_{1}\left({a}\right)\underset{1-1}{⟶}\mathrm{\omega }↔\bigcup _{{a}\in \mathrm{\omega }}\mathrm{rec}\left({G},\varnothing \right)\left({a}\right):\bigcup {R}_{1}\left[\mathrm{\omega }\right]\underset{1-1}{⟶}\mathrm{\omega }\right)$
41 38 39 40 mp2b ${⊢}\bigcup _{{a}\in \mathrm{\omega }}\mathrm{rec}\left({G},\varnothing \right)\left({a}\right):\bigcup _{{a}\in \mathrm{\omega }}{R}_{1}\left({a}\right)\underset{1-1}{⟶}\mathrm{\omega }↔\bigcup _{{a}\in \mathrm{\omega }}\mathrm{rec}\left({G},\varnothing \right)\left({a}\right):\bigcup {R}_{1}\left[\mathrm{\omega }\right]\underset{1-1}{⟶}\mathrm{\omega }$
42 36 41 bitr4i ${⊢}\bigcup \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]:\bigcup {R}_{1}\left[\mathrm{\omega }\right]\underset{1-1}{⟶}\mathrm{\omega }↔\bigcup _{{a}\in \mathrm{\omega }}\mathrm{rec}\left({G},\varnothing \right)\left({a}\right):\bigcup _{{a}\in \mathrm{\omega }}{R}_{1}\left({a}\right)\underset{1-1}{⟶}\mathrm{\omega }$
43 31 42 mpbir ${⊢}\bigcup \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]:\bigcup {R}_{1}\left[\mathrm{\omega }\right]\underset{1-1}{⟶}\mathrm{\omega }$
44 rnuni ${⊢}\mathrm{ran}\bigcup \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]=\bigcup _{{a}\in \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]}\mathrm{ran}{a}$
45 eliun ${⊢}{b}\in \bigcup _{{a}\in \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]}\mathrm{ran}{a}↔\exists {a}\in \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]\phantom{\rule{.4em}{0ex}}{b}\in \mathrm{ran}{a}$
46 df-rex ${⊢}\exists {a}\in \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]\phantom{\rule{.4em}{0ex}}{b}\in \mathrm{ran}{a}↔\exists {a}\phantom{\rule{.4em}{0ex}}\left({a}\in \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]\wedge {b}\in \mathrm{ran}{a}\right)$
47 funfn ${⊢}\mathrm{Fun}\mathrm{rec}\left({G},\varnothing \right)↔\mathrm{rec}\left({G},\varnothing \right)Fn\mathrm{dom}\mathrm{rec}\left({G},\varnothing \right)$
48 32 47 mpbi ${⊢}\mathrm{rec}\left({G},\varnothing \right)Fn\mathrm{dom}\mathrm{rec}\left({G},\varnothing \right)$
49 rdgdmlim ${⊢}\mathrm{Lim}\mathrm{dom}\mathrm{rec}\left({G},\varnothing \right)$
50 limomss ${⊢}\mathrm{Lim}\mathrm{dom}\mathrm{rec}\left({G},\varnothing \right)\to \mathrm{\omega }\subseteq \mathrm{dom}\mathrm{rec}\left({G},\varnothing \right)$
51 49 50 ax-mp ${⊢}\mathrm{\omega }\subseteq \mathrm{dom}\mathrm{rec}\left({G},\varnothing \right)$
52 fvelimab ${⊢}\left(\mathrm{rec}\left({G},\varnothing \right)Fn\mathrm{dom}\mathrm{rec}\left({G},\varnothing \right)\wedge \mathrm{\omega }\subseteq \mathrm{dom}\mathrm{rec}\left({G},\varnothing \right)\right)\to \left({a}\in \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]↔\exists {c}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\mathrm{rec}\left({G},\varnothing \right)\left({c}\right)={a}\right)$
53 48 51 52 mp2an ${⊢}{a}\in \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]↔\exists {c}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\mathrm{rec}\left({G},\varnothing \right)\left({c}\right)={a}$
54 1 2 ackbij2lem2 ${⊢}{c}\in \mathrm{\omega }\to \mathrm{rec}\left({G},\varnothing \right)\left({c}\right):{R}_{1}\left({c}\right)\underset{1-1 onto}{⟶}\mathrm{card}\left({R}_{1}\left({c}\right)\right)$
55 f1ofo ${⊢}\mathrm{rec}\left({G},\varnothing \right)\left({c}\right):{R}_{1}\left({c}\right)\underset{1-1 onto}{⟶}\mathrm{card}\left({R}_{1}\left({c}\right)\right)\to \mathrm{rec}\left({G},\varnothing \right)\left({c}\right):{R}_{1}\left({c}\right)\underset{onto}{⟶}\mathrm{card}\left({R}_{1}\left({c}\right)\right)$
56 forn ${⊢}\mathrm{rec}\left({G},\varnothing \right)\left({c}\right):{R}_{1}\left({c}\right)\underset{onto}{⟶}\mathrm{card}\left({R}_{1}\left({c}\right)\right)\to \mathrm{ran}\mathrm{rec}\left({G},\varnothing \right)\left({c}\right)=\mathrm{card}\left({R}_{1}\left({c}\right)\right)$
57 54 55 56 3syl ${⊢}{c}\in \mathrm{\omega }\to \mathrm{ran}\mathrm{rec}\left({G},\varnothing \right)\left({c}\right)=\mathrm{card}\left({R}_{1}\left({c}\right)\right)$
58 r1fin ${⊢}{c}\in \mathrm{\omega }\to {R}_{1}\left({c}\right)\in \mathrm{Fin}$
59 ficardom ${⊢}{R}_{1}\left({c}\right)\in \mathrm{Fin}\to \mathrm{card}\left({R}_{1}\left({c}\right)\right)\in \mathrm{\omega }$
60 58 59 syl ${⊢}{c}\in \mathrm{\omega }\to \mathrm{card}\left({R}_{1}\left({c}\right)\right)\in \mathrm{\omega }$
61 ordelss ${⊢}\left(\mathrm{Ord}\mathrm{\omega }\wedge \mathrm{card}\left({R}_{1}\left({c}\right)\right)\in \mathrm{\omega }\right)\to \mathrm{card}\left({R}_{1}\left({c}\right)\right)\subseteq \mathrm{\omega }$
62 10 60 61 sylancr ${⊢}{c}\in \mathrm{\omega }\to \mathrm{card}\left({R}_{1}\left({c}\right)\right)\subseteq \mathrm{\omega }$
63 57 62 eqsstrd ${⊢}{c}\in \mathrm{\omega }\to \mathrm{ran}\mathrm{rec}\left({G},\varnothing \right)\left({c}\right)\subseteq \mathrm{\omega }$
64 rneq ${⊢}\mathrm{rec}\left({G},\varnothing \right)\left({c}\right)={a}\to \mathrm{ran}\mathrm{rec}\left({G},\varnothing \right)\left({c}\right)=\mathrm{ran}{a}$
65 64 sseq1d ${⊢}\mathrm{rec}\left({G},\varnothing \right)\left({c}\right)={a}\to \left(\mathrm{ran}\mathrm{rec}\left({G},\varnothing \right)\left({c}\right)\subseteq \mathrm{\omega }↔\mathrm{ran}{a}\subseteq \mathrm{\omega }\right)$
66 63 65 syl5ibcom ${⊢}{c}\in \mathrm{\omega }\to \left(\mathrm{rec}\left({G},\varnothing \right)\left({c}\right)={a}\to \mathrm{ran}{a}\subseteq \mathrm{\omega }\right)$
67 66 rexlimiv ${⊢}\exists {c}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\mathrm{rec}\left({G},\varnothing \right)\left({c}\right)={a}\to \mathrm{ran}{a}\subseteq \mathrm{\omega }$
68 53 67 sylbi ${⊢}{a}\in \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]\to \mathrm{ran}{a}\subseteq \mathrm{\omega }$
69 68 sselda ${⊢}\left({a}\in \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]\wedge {b}\in \mathrm{ran}{a}\right)\to {b}\in \mathrm{\omega }$
70 69 exlimiv ${⊢}\exists {a}\phantom{\rule{.4em}{0ex}}\left({a}\in \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]\wedge {b}\in \mathrm{ran}{a}\right)\to {b}\in \mathrm{\omega }$
71 peano2 ${⊢}{b}\in \mathrm{\omega }\to \mathrm{suc}{b}\in \mathrm{\omega }$
72 fnfvima ${⊢}\left(\mathrm{rec}\left({G},\varnothing \right)Fn\mathrm{dom}\mathrm{rec}\left({G},\varnothing \right)\wedge \mathrm{\omega }\subseteq \mathrm{dom}\mathrm{rec}\left({G},\varnothing \right)\wedge \mathrm{suc}{b}\in \mathrm{\omega }\right)\to \mathrm{rec}\left({G},\varnothing \right)\left(\mathrm{suc}{b}\right)\in \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]$
73 48 51 71 72 mp3an12i ${⊢}{b}\in \mathrm{\omega }\to \mathrm{rec}\left({G},\varnothing \right)\left(\mathrm{suc}{b}\right)\in \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]$
74 vex ${⊢}{b}\in \mathrm{V}$
75 cardnn ${⊢}\mathrm{suc}{b}\in \mathrm{\omega }\to \mathrm{card}\left(\mathrm{suc}{b}\right)=\mathrm{suc}{b}$
76 fvex ${⊢}{R}_{1}\left(\mathrm{suc}{b}\right)\in \mathrm{V}$
77 37 simpri ${⊢}\mathrm{Lim}\mathrm{dom}{R}_{1}$
78 limomss ${⊢}\mathrm{Lim}\mathrm{dom}{R}_{1}\to \mathrm{\omega }\subseteq \mathrm{dom}{R}_{1}$
79 77 78 ax-mp ${⊢}\mathrm{\omega }\subseteq \mathrm{dom}{R}_{1}$
80 79 sseli ${⊢}\mathrm{suc}{b}\in \mathrm{\omega }\to \mathrm{suc}{b}\in \mathrm{dom}{R}_{1}$
81 onssr1 ${⊢}\mathrm{suc}{b}\in \mathrm{dom}{R}_{1}\to \mathrm{suc}{b}\subseteq {R}_{1}\left(\mathrm{suc}{b}\right)$
82 80 81 syl ${⊢}\mathrm{suc}{b}\in \mathrm{\omega }\to \mathrm{suc}{b}\subseteq {R}_{1}\left(\mathrm{suc}{b}\right)$
83 ssdomg ${⊢}{R}_{1}\left(\mathrm{suc}{b}\right)\in \mathrm{V}\to \left(\mathrm{suc}{b}\subseteq {R}_{1}\left(\mathrm{suc}{b}\right)\to \mathrm{suc}{b}\preccurlyeq {R}_{1}\left(\mathrm{suc}{b}\right)\right)$
84 76 82 83 mpsyl ${⊢}\mathrm{suc}{b}\in \mathrm{\omega }\to \mathrm{suc}{b}\preccurlyeq {R}_{1}\left(\mathrm{suc}{b}\right)$
85 nnon ${⊢}\mathrm{suc}{b}\in \mathrm{\omega }\to \mathrm{suc}{b}\in \mathrm{On}$
86 onenon ${⊢}\mathrm{suc}{b}\in \mathrm{On}\to \mathrm{suc}{b}\in \mathrm{dom}\mathrm{card}$
87 85 86 syl ${⊢}\mathrm{suc}{b}\in \mathrm{\omega }\to \mathrm{suc}{b}\in \mathrm{dom}\mathrm{card}$
88 r1fin ${⊢}\mathrm{suc}{b}\in \mathrm{\omega }\to {R}_{1}\left(\mathrm{suc}{b}\right)\in \mathrm{Fin}$
89 finnum ${⊢}{R}_{1}\left(\mathrm{suc}{b}\right)\in \mathrm{Fin}\to {R}_{1}\left(\mathrm{suc}{b}\right)\in \mathrm{dom}\mathrm{card}$
90 88 89 syl ${⊢}\mathrm{suc}{b}\in \mathrm{\omega }\to {R}_{1}\left(\mathrm{suc}{b}\right)\in \mathrm{dom}\mathrm{card}$
91 carddom2 ${⊢}\left(\mathrm{suc}{b}\in \mathrm{dom}\mathrm{card}\wedge {R}_{1}\left(\mathrm{suc}{b}\right)\in \mathrm{dom}\mathrm{card}\right)\to \left(\mathrm{card}\left(\mathrm{suc}{b}\right)\subseteq \mathrm{card}\left({R}_{1}\left(\mathrm{suc}{b}\right)\right)↔\mathrm{suc}{b}\preccurlyeq {R}_{1}\left(\mathrm{suc}{b}\right)\right)$
92 87 90 91 syl2anc ${⊢}\mathrm{suc}{b}\in \mathrm{\omega }\to \left(\mathrm{card}\left(\mathrm{suc}{b}\right)\subseteq \mathrm{card}\left({R}_{1}\left(\mathrm{suc}{b}\right)\right)↔\mathrm{suc}{b}\preccurlyeq {R}_{1}\left(\mathrm{suc}{b}\right)\right)$
93 84 92 mpbird ${⊢}\mathrm{suc}{b}\in \mathrm{\omega }\to \mathrm{card}\left(\mathrm{suc}{b}\right)\subseteq \mathrm{card}\left({R}_{1}\left(\mathrm{suc}{b}\right)\right)$
94 75 93 eqsstrrd ${⊢}\mathrm{suc}{b}\in \mathrm{\omega }\to \mathrm{suc}{b}\subseteq \mathrm{card}\left({R}_{1}\left(\mathrm{suc}{b}\right)\right)$
95 71 94 syl ${⊢}{b}\in \mathrm{\omega }\to \mathrm{suc}{b}\subseteq \mathrm{card}\left({R}_{1}\left(\mathrm{suc}{b}\right)\right)$
96 sucssel ${⊢}{b}\in \mathrm{V}\to \left(\mathrm{suc}{b}\subseteq \mathrm{card}\left({R}_{1}\left(\mathrm{suc}{b}\right)\right)\to {b}\in \mathrm{card}\left({R}_{1}\left(\mathrm{suc}{b}\right)\right)\right)$
97 74 95 96 mpsyl ${⊢}{b}\in \mathrm{\omega }\to {b}\in \mathrm{card}\left({R}_{1}\left(\mathrm{suc}{b}\right)\right)$
98 1 2 ackbij2lem2 ${⊢}\mathrm{suc}{b}\in \mathrm{\omega }\to \mathrm{rec}\left({G},\varnothing \right)\left(\mathrm{suc}{b}\right):{R}_{1}\left(\mathrm{suc}{b}\right)\underset{1-1 onto}{⟶}\mathrm{card}\left({R}_{1}\left(\mathrm{suc}{b}\right)\right)$
99 f1ofo ${⊢}\mathrm{rec}\left({G},\varnothing \right)\left(\mathrm{suc}{b}\right):{R}_{1}\left(\mathrm{suc}{b}\right)\underset{1-1 onto}{⟶}\mathrm{card}\left({R}_{1}\left(\mathrm{suc}{b}\right)\right)\to \mathrm{rec}\left({G},\varnothing \right)\left(\mathrm{suc}{b}\right):{R}_{1}\left(\mathrm{suc}{b}\right)\underset{onto}{⟶}\mathrm{card}\left({R}_{1}\left(\mathrm{suc}{b}\right)\right)$
100 forn ${⊢}\mathrm{rec}\left({G},\varnothing \right)\left(\mathrm{suc}{b}\right):{R}_{1}\left(\mathrm{suc}{b}\right)\underset{onto}{⟶}\mathrm{card}\left({R}_{1}\left(\mathrm{suc}{b}\right)\right)\to \mathrm{ran}\mathrm{rec}\left({G},\varnothing \right)\left(\mathrm{suc}{b}\right)=\mathrm{card}\left({R}_{1}\left(\mathrm{suc}{b}\right)\right)$
101 71 98 99 100 4syl ${⊢}{b}\in \mathrm{\omega }\to \mathrm{ran}\mathrm{rec}\left({G},\varnothing \right)\left(\mathrm{suc}{b}\right)=\mathrm{card}\left({R}_{1}\left(\mathrm{suc}{b}\right)\right)$
102 97 101 eleqtrrd ${⊢}{b}\in \mathrm{\omega }\to {b}\in \mathrm{ran}\mathrm{rec}\left({G},\varnothing \right)\left(\mathrm{suc}{b}\right)$
103 fvex ${⊢}\mathrm{rec}\left({G},\varnothing \right)\left(\mathrm{suc}{b}\right)\in \mathrm{V}$
104 eleq1 ${⊢}{a}=\mathrm{rec}\left({G},\varnothing \right)\left(\mathrm{suc}{b}\right)\to \left({a}\in \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]↔\mathrm{rec}\left({G},\varnothing \right)\left(\mathrm{suc}{b}\right)\in \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]\right)$
105 rneq ${⊢}{a}=\mathrm{rec}\left({G},\varnothing \right)\left(\mathrm{suc}{b}\right)\to \mathrm{ran}{a}=\mathrm{ran}\mathrm{rec}\left({G},\varnothing \right)\left(\mathrm{suc}{b}\right)$
106 105 eleq2d ${⊢}{a}=\mathrm{rec}\left({G},\varnothing \right)\left(\mathrm{suc}{b}\right)\to \left({b}\in \mathrm{ran}{a}↔{b}\in \mathrm{ran}\mathrm{rec}\left({G},\varnothing \right)\left(\mathrm{suc}{b}\right)\right)$
107 104 106 anbi12d ${⊢}{a}=\mathrm{rec}\left({G},\varnothing \right)\left(\mathrm{suc}{b}\right)\to \left(\left({a}\in \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]\wedge {b}\in \mathrm{ran}{a}\right)↔\left(\mathrm{rec}\left({G},\varnothing \right)\left(\mathrm{suc}{b}\right)\in \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]\wedge {b}\in \mathrm{ran}\mathrm{rec}\left({G},\varnothing \right)\left(\mathrm{suc}{b}\right)\right)\right)$
108 103 107 spcev ${⊢}\left(\mathrm{rec}\left({G},\varnothing \right)\left(\mathrm{suc}{b}\right)\in \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]\wedge {b}\in \mathrm{ran}\mathrm{rec}\left({G},\varnothing \right)\left(\mathrm{suc}{b}\right)\right)\to \exists {a}\phantom{\rule{.4em}{0ex}}\left({a}\in \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]\wedge {b}\in \mathrm{ran}{a}\right)$
109 73 102 108 syl2anc ${⊢}{b}\in \mathrm{\omega }\to \exists {a}\phantom{\rule{.4em}{0ex}}\left({a}\in \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]\wedge {b}\in \mathrm{ran}{a}\right)$
110 70 109 impbii ${⊢}\exists {a}\phantom{\rule{.4em}{0ex}}\left({a}\in \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]\wedge {b}\in \mathrm{ran}{a}\right)↔{b}\in \mathrm{\omega }$
111 45 46 110 3bitri ${⊢}{b}\in \bigcup _{{a}\in \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]}\mathrm{ran}{a}↔{b}\in \mathrm{\omega }$
112 111 eqriv ${⊢}\bigcup _{{a}\in \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]}\mathrm{ran}{a}=\mathrm{\omega }$
113 44 112 eqtri ${⊢}\mathrm{ran}\bigcup \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]=\mathrm{\omega }$
114 dff1o5 ${⊢}\bigcup \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]:\bigcup {R}_{1}\left[\mathrm{\omega }\right]\underset{1-1 onto}{⟶}\mathrm{\omega }↔\left(\bigcup \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]:\bigcup {R}_{1}\left[\mathrm{\omega }\right]\underset{1-1}{⟶}\mathrm{\omega }\wedge \mathrm{ran}\bigcup \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]=\mathrm{\omega }\right)$
115 43 113 114 mpbir2an ${⊢}\bigcup \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]:\bigcup {R}_{1}\left[\mathrm{\omega }\right]\underset{1-1 onto}{⟶}\mathrm{\omega }$
116 f1oeq1 ${⊢}{H}=\bigcup \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]\to \left({H}:\bigcup {R}_{1}\left[\mathrm{\omega }\right]\underset{1-1 onto}{⟶}\mathrm{\omega }↔\bigcup \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]:\bigcup {R}_{1}\left[\mathrm{\omega }\right]\underset{1-1 onto}{⟶}\mathrm{\omega }\right)$
117 3 116 ax-mp ${⊢}{H}:\bigcup {R}_{1}\left[\mathrm{\omega }\right]\underset{1-1 onto}{⟶}\mathrm{\omega }↔\bigcup \mathrm{rec}\left({G},\varnothing \right)\left[\mathrm{\omega }\right]:\bigcup {R}_{1}\left[\mathrm{\omega }\right]\underset{1-1 onto}{⟶}\mathrm{\omega }$
118 115 117 mpbir ${⊢}{H}:\bigcup {R}_{1}\left[\mathrm{\omega }\right]\underset{1-1 onto}{⟶}\mathrm{\omega }$