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