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 ran F F -1 A

Proof

Step Hyp Ref Expression
1 elex A ran F A V
2 snprc ¬ A V A =
3 2 biimpi ¬ A V A =
4 3 imaeq2d ¬ A V F -1 A = F -1
5 ima0 F -1 =
6 4 5 syl6eq ¬ A V F -1 A =
7 6 necon1ai F -1 A A V
8 eleq1 a = A a ran F A ran F
9 sneq a = A a = A
10 9 imaeq2d a = A F -1 a = F -1 A
11 10 neeq1d a = A F -1 a F -1 A
12 abn0 b | b F a b b F a
13 iniseg a V F -1 a = b | b F a
14 13 elv F -1 a = b | b F a
15 14 neeq1i F -1 a b | b F a
16 vex a V
17 16 elrn a ran F b b F a
18 12 15 17 3bitr4ri a ran F F -1 a
19 8 11 18 vtoclbg A V A ran F F -1 A
20 1 7 19 pm5.21nii A ran F F -1 A