This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 rgen2 ⊢ ∀ 𝑎 ∈ ω ∀ 𝑏 ∈ ω ( ( 𝐸 ‘ 𝑎 ) = ( 𝐸 ‘ 𝑏 ) → 𝑎 = 𝑏 )
26 dff13 ⊢ ( 𝐸 : ω –1-1→ ω ↔ ( 𝐸 : ω ⟶ ω ∧ ∀ 𝑎 ∈ ω ∀ 𝑏 ∈ ω ( ( 𝐸 ‘ 𝑎 ) = ( 𝐸 ‘ 𝑏 ) → 𝑎 = 𝑏 ) ) )
27 5 25 26 mpbir2an ⊢ 𝐸 : ω –1-1→ ω