# Metamath Proof Explorer

## Theorem fin1a2lem4

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

Ref Expression
Hypothesis fin1a2lem.b ${⊢}{E}=\left({x}\in \mathrm{\omega }⟼{2}_{𝑜}{\cdot }_{𝑜}{x}\right)$
Assertion fin1a2lem4 ${⊢}{E}:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{\omega }$

### Proof

Step Hyp Ref Expression
1 fin1a2lem.b ${⊢}{E}=\left({x}\in \mathrm{\omega }⟼{2}_{𝑜}{\cdot }_{𝑜}{x}\right)$
2 2onn ${⊢}{2}_{𝑜}\in \mathrm{\omega }$
3 nnmcl ${⊢}\left({2}_{𝑜}\in \mathrm{\omega }\wedge {x}\in \mathrm{\omega }\right)\to {2}_{𝑜}{\cdot }_{𝑜}{x}\in \mathrm{\omega }$
4 2 3 mpan ${⊢}{x}\in \mathrm{\omega }\to {2}_{𝑜}{\cdot }_{𝑜}{x}\in \mathrm{\omega }$
5 1 4 fmpti ${⊢}{E}:\mathrm{\omega }⟶\mathrm{\omega }$
6 1 fin1a2lem3 ${⊢}{a}\in \mathrm{\omega }\to {E}\left({a}\right)={2}_{𝑜}{\cdot }_{𝑜}{a}$
7 1 fin1a2lem3 ${⊢}{b}\in \mathrm{\omega }\to {E}\left({b}\right)={2}_{𝑜}{\cdot }_{𝑜}{b}$
8 6 7 eqeqan12d ${⊢}\left({a}\in \mathrm{\omega }\wedge {b}\in \mathrm{\omega }\right)\to \left({E}\left({a}\right)={E}\left({b}\right)↔{2}_{𝑜}{\cdot }_{𝑜}{a}={2}_{𝑜}{\cdot }_{𝑜}{b}\right)$
9 2on ${⊢}{2}_{𝑜}\in \mathrm{On}$
10 9 a1i ${⊢}\left({a}\in \mathrm{\omega }\wedge {b}\in \mathrm{\omega }\right)\to {2}_{𝑜}\in \mathrm{On}$
11 nnon ${⊢}{a}\in \mathrm{\omega }\to {a}\in \mathrm{On}$
12 11 adantr ${⊢}\left({a}\in \mathrm{\omega }\wedge {b}\in \mathrm{\omega }\right)\to {a}\in \mathrm{On}$
13 nnon ${⊢}{b}\in \mathrm{\omega }\to {b}\in \mathrm{On}$
14 13 adantl ${⊢}\left({a}\in \mathrm{\omega }\wedge {b}\in \mathrm{\omega }\right)\to {b}\in \mathrm{On}$
15 0lt1o ${⊢}\varnothing \in {1}_{𝑜}$
16 elelsuc ${⊢}\varnothing \in {1}_{𝑜}\to \varnothing \in \mathrm{suc}{1}_{𝑜}$
17 15 16 ax-mp ${⊢}\varnothing \in \mathrm{suc}{1}_{𝑜}$
18 df-2o ${⊢}{2}_{𝑜}=\mathrm{suc}{1}_{𝑜}$
19 17 18 eleqtrri ${⊢}\varnothing \in {2}_{𝑜}$
20 19 a1i ${⊢}\left({a}\in \mathrm{\omega }\wedge {b}\in \mathrm{\omega }\right)\to \varnothing \in {2}_{𝑜}$
21 omcan ${⊢}\left(\left({2}_{𝑜}\in \mathrm{On}\wedge {a}\in \mathrm{On}\wedge {b}\in \mathrm{On}\right)\wedge \varnothing \in {2}_{𝑜}\right)\to \left({2}_{𝑜}{\cdot }_{𝑜}{a}={2}_{𝑜}{\cdot }_{𝑜}{b}↔{a}={b}\right)$
22 10 12 14 20 21 syl31anc ${⊢}\left({a}\in \mathrm{\omega }\wedge {b}\in \mathrm{\omega }\right)\to \left({2}_{𝑜}{\cdot }_{𝑜}{a}={2}_{𝑜}{\cdot }_{𝑜}{b}↔{a}={b}\right)$
23 8 22 bitrd ${⊢}\left({a}\in \mathrm{\omega }\wedge {b}\in \mathrm{\omega }\right)\to \left({E}\left({a}\right)={E}\left({b}\right)↔{a}={b}\right)$
24 23 biimpd ${⊢}\left({a}\in \mathrm{\omega }\wedge {b}\in \mathrm{\omega }\right)\to \left({E}\left({a}\right)={E}\left({b}\right)\to {a}={b}\right)$
25 24 rgen2 ${⊢}\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({E}\left({a}\right)={E}\left({b}\right)\to {a}={b}\right)$
26 dff13 ${⊢}{E}:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{\omega }↔\left({E}:\mathrm{\omega }⟶\mathrm{\omega }\wedge \forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({E}\left({a}\right)={E}\left({b}\right)\to {a}={b}\right)\right)$
27 5 25 26 mpbir2an ${⊢}{E}:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{\omega }$