# 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 } ) =/= (/) )`