# Metamath Proof Explorer

## Theorem fin1a2lem6

Description: Lemma for fin1a2 . Establish that _om can be broken into two equipollent pieces. (Contributed by Stefan O'Rear, 7-Nov-2014)

Ref Expression
Hypotheses fin1a2lem.b ${⊢}{E}=\left({x}\in \mathrm{\omega }⟼{2}_{𝑜}{\cdot }_{𝑜}{x}\right)$
fin1a2lem.aa ${⊢}{S}=\left({x}\in \mathrm{On}⟼\mathrm{suc}{x}\right)$
Assertion fin1a2lem6 ${⊢}\left({{S}↾}_{\mathrm{ran}{E}}\right):\mathrm{ran}{E}\underset{1-1 onto}{⟶}\mathrm{\omega }\setminus \mathrm{ran}{E}$

### Proof

Step Hyp Ref Expression
1 fin1a2lem.b ${⊢}{E}=\left({x}\in \mathrm{\omega }⟼{2}_{𝑜}{\cdot }_{𝑜}{x}\right)$
2 fin1a2lem.aa ${⊢}{S}=\left({x}\in \mathrm{On}⟼\mathrm{suc}{x}\right)$
3 2 fin1a2lem2 ${⊢}{S}:\mathrm{On}\underset{1-1}{⟶}\mathrm{On}$
4 1 fin1a2lem4 ${⊢}{E}:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{\omega }$
5 f1f ${⊢}{E}:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{\omega }\to {E}:\mathrm{\omega }⟶\mathrm{\omega }$
6 frn ${⊢}{E}:\mathrm{\omega }⟶\mathrm{\omega }\to \mathrm{ran}{E}\subseteq \mathrm{\omega }$
7 omsson ${⊢}\mathrm{\omega }\subseteq \mathrm{On}$
8 6 7 sstrdi ${⊢}{E}:\mathrm{\omega }⟶\mathrm{\omega }\to \mathrm{ran}{E}\subseteq \mathrm{On}$
9 4 5 8 mp2b ${⊢}\mathrm{ran}{E}\subseteq \mathrm{On}$
10 f1ores ${⊢}\left({S}:\mathrm{On}\underset{1-1}{⟶}\mathrm{On}\wedge \mathrm{ran}{E}\subseteq \mathrm{On}\right)\to \left({{S}↾}_{\mathrm{ran}{E}}\right):\mathrm{ran}{E}\underset{1-1 onto}{⟶}{S}\left[\mathrm{ran}{E}\right]$
11 3 9 10 mp2an ${⊢}\left({{S}↾}_{\mathrm{ran}{E}}\right):\mathrm{ran}{E}\underset{1-1 onto}{⟶}{S}\left[\mathrm{ran}{E}\right]$
12 9 sseli ${⊢}{b}\in \mathrm{ran}{E}\to {b}\in \mathrm{On}$
13 2 fin1a2lem1 ${⊢}{b}\in \mathrm{On}\to {S}\left({b}\right)=\mathrm{suc}{b}$
14 12 13 syl ${⊢}{b}\in \mathrm{ran}{E}\to {S}\left({b}\right)=\mathrm{suc}{b}$
15 14 eqeq1d ${⊢}{b}\in \mathrm{ran}{E}\to \left({S}\left({b}\right)={a}↔\mathrm{suc}{b}={a}\right)$
16 15 rexbiia ${⊢}\exists {b}\in \mathrm{ran}{E}\phantom{\rule{.4em}{0ex}}{S}\left({b}\right)={a}↔\exists {b}\in \mathrm{ran}{E}\phantom{\rule{.4em}{0ex}}\mathrm{suc}{b}={a}$
17 4 5 6 mp2b ${⊢}\mathrm{ran}{E}\subseteq \mathrm{\omega }$
18 17 sseli ${⊢}{b}\in \mathrm{ran}{E}\to {b}\in \mathrm{\omega }$
19 peano2 ${⊢}{b}\in \mathrm{\omega }\to \mathrm{suc}{b}\in \mathrm{\omega }$
20 18 19 syl ${⊢}{b}\in \mathrm{ran}{E}\to \mathrm{suc}{b}\in \mathrm{\omega }$
21 1 fin1a2lem5 ${⊢}{b}\in \mathrm{\omega }\to \left({b}\in \mathrm{ran}{E}↔¬\mathrm{suc}{b}\in \mathrm{ran}{E}\right)$
22 21 biimpd ${⊢}{b}\in \mathrm{\omega }\to \left({b}\in \mathrm{ran}{E}\to ¬\mathrm{suc}{b}\in \mathrm{ran}{E}\right)$
23 18 22 mpcom ${⊢}{b}\in \mathrm{ran}{E}\to ¬\mathrm{suc}{b}\in \mathrm{ran}{E}$
24 20 23 jca ${⊢}{b}\in \mathrm{ran}{E}\to \left(\mathrm{suc}{b}\in \mathrm{\omega }\wedge ¬\mathrm{suc}{b}\in \mathrm{ran}{E}\right)$
25 eleq1 ${⊢}\mathrm{suc}{b}={a}\to \left(\mathrm{suc}{b}\in \mathrm{\omega }↔{a}\in \mathrm{\omega }\right)$
26 eleq1 ${⊢}\mathrm{suc}{b}={a}\to \left(\mathrm{suc}{b}\in \mathrm{ran}{E}↔{a}\in \mathrm{ran}{E}\right)$
27 26 notbid ${⊢}\mathrm{suc}{b}={a}\to \left(¬\mathrm{suc}{b}\in \mathrm{ran}{E}↔¬{a}\in \mathrm{ran}{E}\right)$
28 25 27 anbi12d ${⊢}\mathrm{suc}{b}={a}\to \left(\left(\mathrm{suc}{b}\in \mathrm{\omega }\wedge ¬\mathrm{suc}{b}\in \mathrm{ran}{E}\right)↔\left({a}\in \mathrm{\omega }\wedge ¬{a}\in \mathrm{ran}{E}\right)\right)$
29 24 28 syl5ibcom ${⊢}{b}\in \mathrm{ran}{E}\to \left(\mathrm{suc}{b}={a}\to \left({a}\in \mathrm{\omega }\wedge ¬{a}\in \mathrm{ran}{E}\right)\right)$
30 29 rexlimiv ${⊢}\exists {b}\in \mathrm{ran}{E}\phantom{\rule{.4em}{0ex}}\mathrm{suc}{b}={a}\to \left({a}\in \mathrm{\omega }\wedge ¬{a}\in \mathrm{ran}{E}\right)$
31 peano1 ${⊢}\varnothing \in \mathrm{\omega }$
32 1 fin1a2lem3 ${⊢}\varnothing \in \mathrm{\omega }\to {E}\left(\varnothing \right)={2}_{𝑜}{\cdot }_{𝑜}\varnothing$
33 31 32 ax-mp ${⊢}{E}\left(\varnothing \right)={2}_{𝑜}{\cdot }_{𝑜}\varnothing$
34 2on ${⊢}{2}_{𝑜}\in \mathrm{On}$
35 om0 ${⊢}{2}_{𝑜}\in \mathrm{On}\to {2}_{𝑜}{\cdot }_{𝑜}\varnothing =\varnothing$
36 34 35 ax-mp ${⊢}{2}_{𝑜}{\cdot }_{𝑜}\varnothing =\varnothing$
37 33 36 eqtri ${⊢}{E}\left(\varnothing \right)=\varnothing$
38 f1fun ${⊢}{E}:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{\omega }\to \mathrm{Fun}{E}$
39 4 38 ax-mp ${⊢}\mathrm{Fun}{E}$
40 f1dm ${⊢}{E}:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{\omega }\to \mathrm{dom}{E}=\mathrm{\omega }$
41 4 40 ax-mp ${⊢}\mathrm{dom}{E}=\mathrm{\omega }$
42 31 41 eleqtrri ${⊢}\varnothing \in \mathrm{dom}{E}$
43 fvelrn ${⊢}\left(\mathrm{Fun}{E}\wedge \varnothing \in \mathrm{dom}{E}\right)\to {E}\left(\varnothing \right)\in \mathrm{ran}{E}$
44 39 42 43 mp2an ${⊢}{E}\left(\varnothing \right)\in \mathrm{ran}{E}$
45 37 44 eqeltrri ${⊢}\varnothing \in \mathrm{ran}{E}$
46 eleq1 ${⊢}{a}=\varnothing \to \left({a}\in \mathrm{ran}{E}↔\varnothing \in \mathrm{ran}{E}\right)$
47 45 46 mpbiri ${⊢}{a}=\varnothing \to {a}\in \mathrm{ran}{E}$
48 47 necon3bi ${⊢}¬{a}\in \mathrm{ran}{E}\to {a}\ne \varnothing$
49 nnsuc ${⊢}\left({a}\in \mathrm{\omega }\wedge {a}\ne \varnothing \right)\to \exists {b}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{a}=\mathrm{suc}{b}$
50 48 49 sylan2 ${⊢}\left({a}\in \mathrm{\omega }\wedge ¬{a}\in \mathrm{ran}{E}\right)\to \exists {b}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{a}=\mathrm{suc}{b}$
51 eleq1 ${⊢}{a}=\mathrm{suc}{b}\to \left({a}\in \mathrm{\omega }↔\mathrm{suc}{b}\in \mathrm{\omega }\right)$
52 eleq1 ${⊢}{a}=\mathrm{suc}{b}\to \left({a}\in \mathrm{ran}{E}↔\mathrm{suc}{b}\in \mathrm{ran}{E}\right)$
53 52 notbid ${⊢}{a}=\mathrm{suc}{b}\to \left(¬{a}\in \mathrm{ran}{E}↔¬\mathrm{suc}{b}\in \mathrm{ran}{E}\right)$
54 51 53 anbi12d ${⊢}{a}=\mathrm{suc}{b}\to \left(\left({a}\in \mathrm{\omega }\wedge ¬{a}\in \mathrm{ran}{E}\right)↔\left(\mathrm{suc}{b}\in \mathrm{\omega }\wedge ¬\mathrm{suc}{b}\in \mathrm{ran}{E}\right)\right)$
55 54 anbi1d ${⊢}{a}=\mathrm{suc}{b}\to \left(\left(\left({a}\in \mathrm{\omega }\wedge ¬{a}\in \mathrm{ran}{E}\right)\wedge {b}\in \mathrm{\omega }\right)↔\left(\left(\mathrm{suc}{b}\in \mathrm{\omega }\wedge ¬\mathrm{suc}{b}\in \mathrm{ran}{E}\right)\wedge {b}\in \mathrm{\omega }\right)\right)$
56 simplr ${⊢}\left(\left(\mathrm{suc}{b}\in \mathrm{\omega }\wedge ¬\mathrm{suc}{b}\in \mathrm{ran}{E}\right)\wedge {b}\in \mathrm{\omega }\right)\to ¬\mathrm{suc}{b}\in \mathrm{ran}{E}$
57 21 adantl ${⊢}\left(\left(\mathrm{suc}{b}\in \mathrm{\omega }\wedge ¬\mathrm{suc}{b}\in \mathrm{ran}{E}\right)\wedge {b}\in \mathrm{\omega }\right)\to \left({b}\in \mathrm{ran}{E}↔¬\mathrm{suc}{b}\in \mathrm{ran}{E}\right)$
58 56 57 mpbird ${⊢}\left(\left(\mathrm{suc}{b}\in \mathrm{\omega }\wedge ¬\mathrm{suc}{b}\in \mathrm{ran}{E}\right)\wedge {b}\in \mathrm{\omega }\right)\to {b}\in \mathrm{ran}{E}$
59 55 58 syl6bi ${⊢}{a}=\mathrm{suc}{b}\to \left(\left(\left({a}\in \mathrm{\omega }\wedge ¬{a}\in \mathrm{ran}{E}\right)\wedge {b}\in \mathrm{\omega }\right)\to {b}\in \mathrm{ran}{E}\right)$
60 59 com12 ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge ¬{a}\in \mathrm{ran}{E}\right)\wedge {b}\in \mathrm{\omega }\right)\to \left({a}=\mathrm{suc}{b}\to {b}\in \mathrm{ran}{E}\right)$
61 60 impr ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge ¬{a}\in \mathrm{ran}{E}\right)\wedge \left({b}\in \mathrm{\omega }\wedge {a}=\mathrm{suc}{b}\right)\right)\to {b}\in \mathrm{ran}{E}$
62 simprr ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge ¬{a}\in \mathrm{ran}{E}\right)\wedge \left({b}\in \mathrm{\omega }\wedge {a}=\mathrm{suc}{b}\right)\right)\to {a}=\mathrm{suc}{b}$
63 62 eqcomd ${⊢}\left(\left({a}\in \mathrm{\omega }\wedge ¬{a}\in \mathrm{ran}{E}\right)\wedge \left({b}\in \mathrm{\omega }\wedge {a}=\mathrm{suc}{b}\right)\right)\to \mathrm{suc}{b}={a}$
64 50 61 63 reximssdv ${⊢}\left({a}\in \mathrm{\omega }\wedge ¬{a}\in \mathrm{ran}{E}\right)\to \exists {b}\in \mathrm{ran}{E}\phantom{\rule{.4em}{0ex}}\mathrm{suc}{b}={a}$
65 30 64 impbii ${⊢}\exists {b}\in \mathrm{ran}{E}\phantom{\rule{.4em}{0ex}}\mathrm{suc}{b}={a}↔\left({a}\in \mathrm{\omega }\wedge ¬{a}\in \mathrm{ran}{E}\right)$
66 16 65 bitri ${⊢}\exists {b}\in \mathrm{ran}{E}\phantom{\rule{.4em}{0ex}}{S}\left({b}\right)={a}↔\left({a}\in \mathrm{\omega }\wedge ¬{a}\in \mathrm{ran}{E}\right)$
67 f1fn ${⊢}{S}:\mathrm{On}\underset{1-1}{⟶}\mathrm{On}\to {S}Fn\mathrm{On}$
68 3 67 ax-mp ${⊢}{S}Fn\mathrm{On}$
69 fvelimab ${⊢}\left({S}Fn\mathrm{On}\wedge \mathrm{ran}{E}\subseteq \mathrm{On}\right)\to \left({a}\in {S}\left[\mathrm{ran}{E}\right]↔\exists {b}\in \mathrm{ran}{E}\phantom{\rule{.4em}{0ex}}{S}\left({b}\right)={a}\right)$
70 68 9 69 mp2an ${⊢}{a}\in {S}\left[\mathrm{ran}{E}\right]↔\exists {b}\in \mathrm{ran}{E}\phantom{\rule{.4em}{0ex}}{S}\left({b}\right)={a}$
71 eldif ${⊢}{a}\in \left(\mathrm{\omega }\setminus \mathrm{ran}{E}\right)↔\left({a}\in \mathrm{\omega }\wedge ¬{a}\in \mathrm{ran}{E}\right)$
72 66 70 71 3bitr4i ${⊢}{a}\in {S}\left[\mathrm{ran}{E}\right]↔{a}\in \left(\mathrm{\omega }\setminus \mathrm{ran}{E}\right)$
73 72 eqriv ${⊢}{S}\left[\mathrm{ran}{E}\right]=\mathrm{\omega }\setminus \mathrm{ran}{E}$
74 f1oeq3 ${⊢}{S}\left[\mathrm{ran}{E}\right]=\mathrm{\omega }\setminus \mathrm{ran}{E}\to \left(\left({{S}↾}_{\mathrm{ran}{E}}\right):\mathrm{ran}{E}\underset{1-1 onto}{⟶}{S}\left[\mathrm{ran}{E}\right]↔\left({{S}↾}_{\mathrm{ran}{E}}\right):\mathrm{ran}{E}\underset{1-1 onto}{⟶}\mathrm{\omega }\setminus \mathrm{ran}{E}\right)$
75 73 74 ax-mp ${⊢}\left({{S}↾}_{\mathrm{ran}{E}}\right):\mathrm{ran}{E}\underset{1-1 onto}{⟶}{S}\left[\mathrm{ran}{E}\right]↔\left({{S}↾}_{\mathrm{ran}{E}}\right):\mathrm{ran}{E}\underset{1-1 onto}{⟶}\mathrm{\omega }\setminus \mathrm{ran}{E}$
76 11 75 mpbi ${⊢}\left({{S}↾}_{\mathrm{ran}{E}}\right):\mathrm{ran}{E}\underset{1-1 onto}{⟶}\mathrm{\omega }\setminus \mathrm{ran}{E}$