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 𝑆 ) → 𝐹 = ( 𝑆 × { ( 𝐹𝑋 ) } ) )