# Metamath Proof Explorer

## Theorem fin1a2lem4

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

Ref Expression
Hypothesis fin1a2lem.b 𝐸 = ( 𝑥 ∈ ω ↦ ( 2o ·o 𝑥 ) )
Assertion fin1a2lem4 𝐸 : ω –1-1→ ω

### Proof

Step Hyp Ref Expression
1 fin1a2lem.b 𝐸 = ( 𝑥 ∈ ω ↦ ( 2o ·o 𝑥 ) )
2 2onn 2o ∈ ω
3 nnmcl ( ( 2o ∈ ω ∧ 𝑥 ∈ ω ) → ( 2o ·o 𝑥 ) ∈ ω )
4 2 3 mpan ( 𝑥 ∈ ω → ( 2o ·o 𝑥 ) ∈ ω )
5 1 4 fmpti 𝐸 : ω ⟶ ω
6 1 fin1a2lem3 ( 𝑎 ∈ ω → ( 𝐸𝑎 ) = ( 2o ·o 𝑎 ) )
7 1 fin1a2lem3 ( 𝑏 ∈ ω → ( 𝐸𝑏 ) = ( 2o ·o 𝑏 ) )
8 6 7 eqeqan12d ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( ( 𝐸𝑎 ) = ( 𝐸𝑏 ) ↔ ( 2o ·o 𝑎 ) = ( 2o ·o 𝑏 ) ) )
9 2on 2o ∈ On
10 9 a1i ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → 2o ∈ On )
11 nnon ( 𝑎 ∈ ω → 𝑎 ∈ On )
12 11 adantr ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → 𝑎 ∈ On )
13 nnon ( 𝑏 ∈ ω → 𝑏 ∈ On )
14 13 adantl ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → 𝑏 ∈ On )
15 0lt1o ∅ ∈ 1o
16 elelsuc ( ∅ ∈ 1o → ∅ ∈ suc 1o )
17 15 16 ax-mp ∅ ∈ suc 1o
18 df-2o 2o = suc 1o
19 17 18 eleqtrri ∅ ∈ 2o
20 19 a1i ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ∅ ∈ 2o )
21 omcan ( ( ( 2o ∈ On ∧ 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ∅ ∈ 2o ) → ( ( 2o ·o 𝑎 ) = ( 2o ·o 𝑏 ) ↔ 𝑎 = 𝑏 ) )
22 10 12 14 20 21 syl31anc ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( ( 2o ·o 𝑎 ) = ( 2o ·o 𝑏 ) ↔ 𝑎 = 𝑏 ) )
23 8 22 bitrd ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( ( 𝐸𝑎 ) = ( 𝐸𝑏 ) ↔ 𝑎 = 𝑏 ) )
24 23 biimpd ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( ( 𝐸𝑎 ) = ( 𝐸𝑏 ) → 𝑎 = 𝑏 ) )
25 24 rgen2a 𝑎 ∈ ω ∀ 𝑏 ∈ ω ( ( 𝐸𝑎 ) = ( 𝐸𝑏 ) → 𝑎 = 𝑏 )
26 dff13 ( 𝐸 : ω –1-1→ ω ↔ ( 𝐸 : ω ⟶ ω ∧ ∀ 𝑎 ∈ ω ∀ 𝑏 ∈ ω ( ( 𝐸𝑎 ) = ( 𝐸𝑏 ) → 𝑎 = 𝑏 ) ) )
27 5 25 26 mpbir2an 𝐸 : ω –1-1→ ω