This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtrdi ⊢ ( ¬ 𝐴 ∈ 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 𝐹 ↔ ( ◡ 𝐹 “ { 𝐴 } ) ≠ ∅ )