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