Theorem fvrn0

Description: A function value is a member of the range plus null. (Contributed by Scott Fenton, 8-Jun-2011) (Revised by Stefan O'Rear, 3-Jan-2015)

	Ref	Expression
Assertion	fvrn0	⊢ ( 𝐹 ‘ 𝑋 ) ∈ ( ran 𝐹 ∪ { ∅ } )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( ( 𝐹 ‘ 𝑋 ) = ∅ → ( 𝐹 ‘ 𝑋 ) = ∅ )
2		ssun2	⊢ { ∅ } ⊆ ( ran 𝐹 ∪ { ∅ } )
3		0ex	⊢ ∅ ∈ V
4	3	snid	⊢ ∅ ∈ { ∅ }
5	2 4	sselii	⊢ ∅ ∈ ( ran 𝐹 ∪ { ∅ } )
6	1 5	eqeltrdi	⊢ ( ( 𝐹 ‘ 𝑋 ) = ∅ → ( 𝐹 ‘ 𝑋 ) ∈ ( ran 𝐹 ∪ { ∅ } ) )
7		ssun1	⊢ ran 𝐹 ⊆ ( ran 𝐹 ∪ { ∅ } )
8		fvprc	⊢ ( ¬ 𝑋 ∈ V → ( 𝐹 ‘ 𝑋 ) = ∅ )
9	8	con1i	⊢ ( ¬ ( 𝐹 ‘ 𝑋 ) = ∅ → 𝑋 ∈ V )
10		fvexd	⊢ ( ¬ ( 𝐹 ‘ 𝑋 ) = ∅ → ( 𝐹 ‘ 𝑋 ) ∈ V )
11		fvbr0	⊢ ( 𝑋 𝐹 ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑋 ) = ∅ )
12	11	ori	⊢ ( ¬ 𝑋 𝐹 ( 𝐹 ‘ 𝑋 ) → ( 𝐹 ‘ 𝑋 ) = ∅ )
13	12	con1i	⊢ ( ¬ ( 𝐹 ‘ 𝑋 ) = ∅ → 𝑋 𝐹 ( 𝐹 ‘ 𝑋 ) )
14		brelrng	⊢ ( ( 𝑋 ∈ V ∧ ( 𝐹 ‘ 𝑋 ) ∈ V ∧ 𝑋 𝐹 ( 𝐹 ‘ 𝑋 ) ) → ( 𝐹 ‘ 𝑋 ) ∈ ran 𝐹 )
15	9 10 13 14	syl3anc	⊢ ( ¬ ( 𝐹 ‘ 𝑋 ) = ∅ → ( 𝐹 ‘ 𝑋 ) ∈ ran 𝐹 )
16	7 15	sseldi	⊢ ( ¬ ( 𝐹 ‘ 𝑋 ) = ∅ → ( 𝐹 ‘ 𝑋 ) ∈ ( ran 𝐹 ∪ { ∅ } ) )
17	6 16	pm2.61i	⊢ ( 𝐹 ‘ 𝑋 ) ∈ ( ran 𝐹 ∪ { ∅ } )