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 ≠ ∅