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→ ω