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

Metamath Proof Explorer

Theorem inisegn0

Description: Nonemptiness of an initial segment in terms of range. (Contributed by Stefan O'Rear, 18-Jan-2015)

Ref Expression
Assertion inisegn0 
|- ( A e. ran F <-> ( `' F " { A } ) =/= (/) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. ran F -> A e. _V )
2 snprc 
 |-  ( -. A e. _V <-> { A } = (/) )
3 2 biimpi 
 |-  ( -. A e. _V -> { A } = (/) )
4 3 imaeq2d 
 |-  ( -. A e. _V -> ( `' F " { A } ) = ( `' F " (/) ) )
5 ima0 
 |-  ( `' F " (/) ) = (/)
6 4 5 eqtrdi 
 |-  ( -. A e. _V -> ( `' F " { A } ) = (/) )
7 6 necon1ai 
 |-  ( ( `' F " { A } ) =/= (/) -> A e. _V )
8 eleq1 
 |-  ( a = A -> ( a e. ran F <-> A e. ran F ) )
9 sneq 
 |-  ( a = A -> { a } = { A } )
10 9 imaeq2d 
 |-  ( a = A -> ( `' F " { a } ) = ( `' F " { A } ) )
11 10 neeq1d 
 |-  ( a = A -> ( ( `' F " { a } ) =/= (/) <-> ( `' F " { A } ) =/= (/) ) )
12 abn0 
 |-  ( { b | b F a } =/= (/) <-> E. b b F a )
13 iniseg 
 |-  ( a e. _V -> ( `' F " { a } ) = { b | b F a } )
14 13 elv 
 |-  ( `' F " { a } ) = { b | b F a }
15 14 neeq1i 
 |-  ( ( `' F " { a } ) =/= (/) <-> { b | b F a } =/= (/) )
16 vex 
 |-  a e. _V
17 16 elrn 
 |-  ( a e. ran F <-> E. b b F a )
18 12 15 17 3bitr4ri 
 |-  ( a e. ran F <-> ( `' F " { a } ) =/= (/) )
19 8 11 18 vtoclbg 
 |-  ( A e. _V -> ( A e. ran F <-> ( `' F " { A } ) =/= (/) ) )
20 1 7 19 pm5.21nii 
 |-  ( A e. ran F <-> ( `' F " { A } ) =/= (/) )