Theorem fin1a2lem5

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	fin1a2lem5	|- ( A e. _om -> ( A e. ran E <-> -. suc A e. ran E ) )

Proof

Step	Hyp	Ref	Expression
1		fin1a2lem.b	|- E = ( x e. _om |-> ( 2o .o x ) )
2		nneob	|- ( A e. _om -> ( E. a e. _om A = ( 2o .o a ) <-> -. E. a e. _om suc A = ( 2o .o a ) ) )
3	1	fin1a2lem4	|- E : _om -1-1-> _om
4		f1fn	|- ( E : _om -1-1-> _om -> E Fn _om )
5	3 4	ax-mp	|- E Fn _om
6		fvelrnb	|- ( E Fn _om -> ( A e. ran E <-> E. a e. _om ( E ` a ) = A ) )
7	5 6	ax-mp	|- ( A e. ran E <-> E. a e. _om ( E ` a ) = A )
8		eqcom	|- ( ( E ` a ) = A <-> A = ( E ` a ) )
9	1	fin1a2lem3	|- ( a e. _om -> ( E ` a ) = ( 2o .o a ) )
10	9	eqeq2d	|- ( a e. _om -> ( A = ( E ` a ) <-> A = ( 2o .o a ) ) )
11	8 10	syl5bb	|- ( a e. _om -> ( ( E ` a ) = A <-> A = ( 2o .o a ) ) )
12	11	rexbiia	|- ( E. a e. _om ( E ` a ) = A <-> E. a e. _om A = ( 2o .o a ) )
13	7 12	bitri	|- ( A e. ran E <-> E. a e. _om A = ( 2o .o a ) )
14		fvelrnb	|- ( E Fn _om -> ( suc A e. ran E <-> E. a e. _om ( E ` a ) = suc A ) )
15	5 14	ax-mp	|- ( suc A e. ran E <-> E. a e. _om ( E ` a ) = suc A )
16		eqcom	|- ( ( E ` a ) = suc A <-> suc A = ( E ` a ) )
17	9	eqeq2d	|- ( a e. _om -> ( suc A = ( E ` a ) <-> suc A = ( 2o .o a ) ) )
18	16 17	syl5bb	|- ( a e. _om -> ( ( E ` a ) = suc A <-> suc A = ( 2o .o a ) ) )
19	18	rexbiia	|- ( E. a e. _om ( E ` a ) = suc A <-> E. a e. _om suc A = ( 2o .o a ) )
20	15 19	bitri	|- ( suc A e. ran E <-> E. a e. _om suc A = ( 2o .o a ) )
21	20	notbii	|- ( -. suc A e. ran E <-> -. E. a e. _om suc A = ( 2o .o a ) )
22	2 13 21	3bitr4g	|- ( A e. _om -> ( A e. ran E <-> -. suc A e. ran E ) )