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 AranFF-1A

Proof

Step Hyp Ref Expression
1 elex AranFAV
2 snprc ¬AVA=
3 2 biimpi ¬AVA=
4 3 imaeq2d ¬AVF-1A=F-1
5 ima0 F-1=
6 4 5 eqtrdi ¬AVF-1A=
7 6 necon1ai F-1AAV
8 eleq1 a=AaranFAranF
9 sneq a=Aa=A
10 9 imaeq2d a=AF-1a=F-1A
11 10 neeq1d a=AF-1aF-1A
12 abn0 b|bFabbFa
13 iniseg aVF-1a=b|bFa
14 13 elv F-1a=b|bFa
15 14 neeq1i F-1ab|bFa
16 vex aV
17 16 elrn aranFbbFa
18 12 15 17 3bitr4ri aranFF-1a
19 8 11 18 vtoclbg AVAranFF-1A
20 1 7 19 pm5.21nii AranFF-1A