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

Metamath Proof Explorer

Theorem mapsnconst

Description: Every singleton map is a constant function. (Contributed by Stefan O'Rear, 25-Mar-2015)

Ref Expression
Hypotheses mapsncnv.s ⊢ 𝑆 = { 𝑋 }
mapsncnv.b ⊢ 𝐵 ∈ V
mapsncnv.x ⊢ 𝑋 ∈ V
Assertion mapsnconst ( 𝐹 ∈ ( 𝐵 ↑m 𝑆 ) → 𝐹 = ( 𝑆 × { ( 𝐹 ‘ 𝑋 ) } ) )

Proof

Step Hyp Ref Expression
1 mapsncnv.s ⊢ 𝑆 = { 𝑋 }
2 mapsncnv.b ⊢ 𝐵 ∈ V
3 mapsncnv.x ⊢ 𝑋 ∈ V
4 snex ⊢ { 𝑋 } ∈ V
5 2 4 elmap ⊢ ( 𝐹 ∈ ( 𝐵 ↑m { 𝑋 } ) ↔ 𝐹 : { 𝑋 } ⟶ 𝐵 )
6 3 fsn2 ⊢ ( 𝐹 : { 𝑋 } ⟶ 𝐵 ↔ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 ∧ 𝐹 = { ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) )
7 6 simprbi ⊢ ( 𝐹 : { 𝑋 } ⟶ 𝐵 → 𝐹 = { ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ } )
8 1 xpeq1i ⊢ ( 𝑆 × { ( 𝐹 ‘ 𝑋 ) } ) = ( { 𝑋 } × { ( 𝐹 ‘ 𝑋 ) } )
9 fvex ⊢ ( 𝐹 ‘ 𝑋 ) ∈ V
10 3 9 xpsn ⊢ ( { 𝑋 } × { ( 𝐹 ‘ 𝑋 ) } ) = { ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ }
11 8 10 eqtr2i ⊢ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ } = ( 𝑆 × { ( 𝐹 ‘ 𝑋 ) } )
12 7 11 eqtrdi ⊢ ( 𝐹 : { 𝑋 } ⟶ 𝐵 → 𝐹 = ( 𝑆 × { ( 𝐹 ‘ 𝑋 ) } ) )
13 5 12 sylbi ⊢ ( 𝐹 ∈ ( 𝐵 ↑m { 𝑋 } ) → 𝐹 = ( 𝑆 × { ( 𝐹 ‘ 𝑋 ) } ) )
14 1 oveq2i ⊢ ( 𝐵 ↑m 𝑆 ) = ( 𝐵 ↑m { 𝑋 } )
15 13 14 eleq2s ⊢ ( 𝐹 ∈ ( 𝐵 ↑m 𝑆 ) → 𝐹 = ( 𝑆 × { ( 𝐹 ‘ 𝑋 ) } ) )