# 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 eqtrdi $⊢ ¬ 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 ≠ ∅$