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 ( 𝐹 ‘ 𝑋 ) ∈ ( 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 sselid ⊢ ( ¬ ( 𝐹 ‘ 𝑋 ) = ∅ → ( 𝐹 ‘ 𝑋 ) ∈ ( ran 𝐹 ∪ { ∅ } ) )
17 6 16 pm2.61i ⊢ ( 𝐹 ‘ 𝑋 ) ∈ ( ran 𝐹 ∪ { ∅ } )