Metamath Proof Explorer

Theorem fin1a2lem4

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

Ref Expression
Hypothesis fin1a2lem.b ⊢ E = x ∈ ω ⟼ 2 𝑜 ⋅ 𝑜 x
Assertion fin1a2lem4 ⊢ E : ω ⟶ 1-1 ω

Proof

Step Hyp Ref Expression
1 fin1a2lem.b ⊢ E = x ∈ ω ⟼ 2 𝑜 ⋅ 𝑜 x
2 2onn ⊢ 2 𝑜 ∈ ω
3 nnmcl ⊢ 2 𝑜 ∈ ω ∧ x ∈ ω → 2 𝑜 ⋅ 𝑜 x ∈ ω
4 2 3 mpan ⊢ x ∈ ω → 2 𝑜 ⋅ 𝑜 x ∈ ω
5 1 4 fmpti ⊢ E : ω ⟶ ω
6 1 fin1a2lem3 ⊢ a ∈ ω → E ⁡ a = 2 𝑜 ⋅ 𝑜 a
7 1 fin1a2lem3 ⊢ b ∈ ω → E ⁡ b = 2 𝑜 ⋅ 𝑜 b
8 6 7 eqeqan12d ⊢ a ∈ ω ∧ b ∈ ω → E ⁡ a = E ⁡ b ↔ 2 𝑜 ⋅ 𝑜 a = 2 𝑜 ⋅ 𝑜 b
9 2on ⊢ 2 𝑜 ∈ On
10 9 a1i ⊢ a ∈ ω ∧ b ∈ ω → 2 𝑜 ∈ On
11 nnon ⊢ a ∈ ω → a ∈ On
12 11 adantr ⊢ a ∈ ω ∧ b ∈ ω → a ∈ On
13 nnon ⊢ b ∈ ω → b ∈ On
14 13 adantl ⊢ a ∈ ω ∧ b ∈ ω → b ∈ On
15 0lt1o ⊢ ∅ ∈ 1 𝑜
16 elelsuc ⊢ ∅ ∈ 1 𝑜 → ∅ ∈ suc ⁡ 1 𝑜
17 15 16 ax-mp ⊢ ∅ ∈ suc ⁡ 1 𝑜
18 df-2o ⊢ 2 𝑜 = suc ⁡ 1 𝑜
19 17 18 eleqtrri ⊢ ∅ ∈ 2 𝑜
20 19 a1i ⊢ a ∈ ω ∧ b ∈ ω → ∅ ∈ 2 𝑜
21 omcan ⊢ 2 𝑜 ∈ On ∧ a ∈ On ∧ b ∈ On ∧ ∅ ∈ 2 𝑜 → 2 𝑜 ⋅ 𝑜 a = 2 𝑜 ⋅ 𝑜 b ↔ a = b
22 10 12 14 20 21 syl31anc ⊢ a ∈ ω ∧ b ∈ ω → 2 𝑜 ⋅ 𝑜 a = 2 𝑜 ⋅ 𝑜 b ↔ a = b
23 8 22 bitrd ⊢ a ∈ ω ∧ b ∈ ω → E ⁡ a = E ⁡ b ↔ a = b
24 23 biimpd ⊢ a ∈ ω ∧ b ∈ ω → E ⁡ a = E ⁡ b → a = b
25 24 rgen2 ⊢ ∀ a ∈ ω ∀ b ∈ ω E ⁡ a = E ⁡ b → a = b
26 dff13 ⊢ E : ω ⟶ 1-1 ω ↔ E : ω ⟶ ω ∧ ∀ a ∈ ω ∀ b ∈ ω E ⁡ a = E ⁡ b → a = b
27 5 25 26 mpbir2an ⊢ E : ω ⟶ 1-1 ω