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

Metamath Proof Explorer

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 bitrid 
 |-  ( 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 bitrid 
 |-  ( 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 ) )