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