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 ( 𝐴 ∈ ran 𝐹 ↔ ( 𝐹 “ { 𝐴 } ) ≠ ∅ )

Proof

Step Hyp Ref Expression
1 elex ( 𝐴 ∈ ran 𝐹𝐴 ∈ V )
2 snprc ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
3 2 biimpi ( ¬ 𝐴 ∈ V → { 𝐴 } = ∅ )
4 3 imaeq2d ( ¬ 𝐴 ∈ V → ( 𝐹 “ { 𝐴 } ) = ( 𝐹 “ ∅ ) )
5 ima0 ( 𝐹 “ ∅ ) = ∅
6 4 5 syl6eq ( ¬ 𝐴 ∈ V → ( 𝐹 “ { 𝐴 } ) = ∅ )
7 6 necon1ai ( ( 𝐹 “ { 𝐴 } ) ≠ ∅ → 𝐴 ∈ V )
8 eleq1 ( 𝑎 = 𝐴 → ( 𝑎 ∈ ran 𝐹𝐴 ∈ ran 𝐹 ) )
9 sneq ( 𝑎 = 𝐴 → { 𝑎 } = { 𝐴 } )
10 9 imaeq2d ( 𝑎 = 𝐴 → ( 𝐹 “ { 𝑎 } ) = ( 𝐹 “ { 𝐴 } ) )
11 10 neeq1d ( 𝑎 = 𝐴 → ( ( 𝐹 “ { 𝑎 } ) ≠ ∅ ↔ ( 𝐹 “ { 𝐴 } ) ≠ ∅ ) )
12 abn0 ( { 𝑏𝑏 𝐹 𝑎 } ≠ ∅ ↔ ∃ 𝑏 𝑏 𝐹 𝑎 )
13 iniseg ( 𝑎 ∈ V → ( 𝐹 “ { 𝑎 } ) = { 𝑏𝑏 𝐹 𝑎 } )
14 13 elv ( 𝐹 “ { 𝑎 } ) = { 𝑏𝑏 𝐹 𝑎 }
15 14 neeq1i ( ( 𝐹 “ { 𝑎 } ) ≠ ∅ ↔ { 𝑏𝑏 𝐹 𝑎 } ≠ ∅ )
16 vex 𝑎 ∈ V
17 16 elrn ( 𝑎 ∈ ran 𝐹 ↔ ∃ 𝑏 𝑏 𝐹 𝑎 )
18 12 15 17 3bitr4ri ( 𝑎 ∈ ran 𝐹 ↔ ( 𝐹 “ { 𝑎 } ) ≠ ∅ )
19 8 11 18 vtoclbg ( 𝐴 ∈ V → ( 𝐴 ∈ ran 𝐹 ↔ ( 𝐹 “ { 𝐴 } ) ≠ ∅ ) )
20 1 7 19 pm5.21nii ( 𝐴 ∈ ran 𝐹 ↔ ( 𝐹 “ { 𝐴 } ) ≠ ∅ )