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

Metamath Proof Explorer

Theorem rnsnf

Description: The range of a function whose domain is a singleton. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses rnsnf.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
rnsnf.2 ⊢ ( 𝜑 → 𝐹 : { 𝐴 } ⟶ 𝐵 )
Assertion rnsnf ( 𝜑 → ran 𝐹 = { ( 𝐹 ‘ 𝐴 ) } )

Proof

Step Hyp Ref Expression
1 rnsnf.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 rnsnf.2 ⊢ ( 𝜑 → 𝐹 : { 𝐴 } ⟶ 𝐵 )
3 elsni ⊢ ( 𝑥 ∈ { 𝐴 } → 𝑥 = 𝐴 )
4 3 fveq2d ⊢ ( 𝑥 ∈ { 𝐴 } → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 ) )
5 4 mpteq2ia ⊢ ( 𝑥 ∈ { 𝐴 } ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ { 𝐴 } ↦ ( 𝐹 ‘ 𝐴 ) )
6 2 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ { 𝐴 } ↦ ( 𝐹 ‘ 𝑥 ) ) )
7 fvexd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ V )
8 fmptsn ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ∈ V ) → { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } = ( 𝑥 ∈ { 𝐴 } ↦ ( 𝐹 ‘ 𝐴 ) ) )
9 1 7 8 syl2anc ⊢ ( 𝜑 → { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } = ( 𝑥 ∈ { 𝐴 } ↦ ( 𝐹 ‘ 𝐴 ) ) )
10 5 6 9 3eqtr4a ⊢ ( 𝜑 → 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } )
11 10 rneqd ⊢ ( 𝜑 → ran 𝐹 = ran { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } )
12 rnsnopg ⊢ ( 𝐴 ∈ 𝑉 → ran { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } = { ( 𝐹 ‘ 𝐴 ) } )
13 1 12 syl ⊢ ( 𝜑 → ran { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } = { ( 𝐹 ‘ 𝐴 ) } )
14 11 13 eqtrd ⊢ ( 𝜑 → ran 𝐹 = { ( 𝐹 ‘ 𝐴 ) } )