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

Metamath Proof Explorer

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 ⊢ F ⁡ X ∈ ran ⁡ F ∪ ∅

Proof

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