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 syl6eq
 |-  ( -. 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 } ) =/= (/) )