Theorem fin1a2lem4

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

	Ref	Expression
Hypothesis	fin1a2lem.b	|- E = ( x e. _om |-> ( 2o .o x ) )
Assertion	fin1a2lem4	|- E : _om -1-1-> _om

Proof

Step	Hyp	Ref	Expression
1		fin1a2lem.b	|- E = ( x e. _om |-> ( 2o .o x ) )
2		2onn	|- 2o e. _om
3		nnmcl	|- ( ( 2o e. _om /\ x e. _om ) -> ( 2o .o x ) e. _om )
4	2 3	mpan	|- ( x e. _om -> ( 2o .o x ) e. _om )
5	1 4	fmpti	|- E : _om --> _om
6	1	fin1a2lem3	|- ( a e. _om -> ( E ` a ) = ( 2o .o a ) )
7	1	fin1a2lem3	|- ( b e. _om -> ( E ` b ) = ( 2o .o b ) )
8	6 7	eqeqan12d	|- ( ( a e. _om /\ b e. _om ) -> ( ( E ` a ) = ( E ` b ) <-> ( 2o .o a ) = ( 2o .o b ) ) )
9		2on	|- 2o e. On
10	9	a1i	|- ( ( a e. _om /\ b e. _om ) -> 2o e. On )
11		nnon	|- ( a e. _om -> a e. On )
12	11	adantr	|- ( ( a e. _om /\ b e. _om ) -> a e. On )
13		nnon	|- ( b e. _om -> b e. On )
14	13	adantl	|- ( ( a e. _om /\ b e. _om ) -> b e. On )
15		0lt1o	|- (/) e. 1o
16		elelsuc	|- ( (/) e. 1o -> (/) e. suc 1o )
17	15 16	ax-mp	|- (/) e. suc 1o
18		df-2o	|- 2o = suc 1o
19	17 18	eleqtrri	|- (/) e. 2o
20	19	a1i	|- ( ( a e. _om /\ b e. _om ) -> (/) e. 2o )
21		omcan	|- ( ( ( 2o e. On /\ a e. On /\ b e. On ) /\ (/) e. 2o ) -> ( ( 2o .o a ) = ( 2o .o b ) <-> a = b ) )
22	10 12 14 20 21	syl31anc	|- ( ( a e. _om /\ b e. _om ) -> ( ( 2o .o a ) = ( 2o .o b ) <-> a = b ) )
23	8 22	bitrd	|- ( ( a e. _om /\ b e. _om ) -> ( ( E ` a ) = ( E ` b ) <-> a = b ) )
24	23	biimpd	|- ( ( a e. _om /\ b e. _om ) -> ( ( E ` a ) = ( E ` b ) -> a = b ) )
25	24	rgen2	|- A. a e. _om A. b e. _om ( ( E ` a ) = ( E ` b ) -> a = b )
26		dff13	|- ( E : _om -1-1-> _om <-> ( E : _om --> _om /\ A. a e. _om A. b e. _om ( ( E ` a ) = ( E ` b ) -> a = b ) ) )
27	5 25 26	mpbir2an	|- E : _om -1-1-> _om