Theorem mapsnf1o2

Description: Explicit bijection between a set and its singleton functions. (Contributed by Stefan O'Rear, 21-Mar-2015)

	Ref	Expression
Hypotheses	mapsncnv.s	⊢ 𝑆 = { 𝑋 }
	mapsncnv.b	⊢ 𝐵 ∈ V
	mapsncnv.x	⊢ 𝑋 ∈ V
	mapsncnv.f	⊢ 𝐹 = ( 𝑥 ∈ ( 𝐵 ↑m 𝑆 ) ↦ ( 𝑥 ‘ 𝑋 ) )
Assertion	mapsnf1o2	⊢ 𝐹 : ( 𝐵 ↑m 𝑆 ) –1-1-onto→ 𝐵

Proof

Step	Hyp	Ref	Expression
1		mapsncnv.s	⊢ 𝑆 = { 𝑋 }
2		mapsncnv.b	⊢ 𝐵 ∈ V
3		mapsncnv.x	⊢ 𝑋 ∈ V
4		mapsncnv.f	⊢ 𝐹 = ( 𝑥 ∈ ( 𝐵 ↑m 𝑆 ) ↦ ( 𝑥 ‘ 𝑋 ) )
5		fvex	⊢ ( 𝑥 ‘ 𝑋 ) ∈ V
6	5 4	fnmpti	⊢ 𝐹 Fn ( 𝐵 ↑m 𝑆 )
7		snex	⊢ { 𝑋 } ∈ V
8	1 7	eqeltri	⊢ 𝑆 ∈ V
9		snex	⊢ { 𝑦 } ∈ V
10	8 9	xpex	⊢ ( 𝑆 × { 𝑦 } ) ∈ V
11	1 2 3 4	mapsncnv	⊢ ◡ 𝐹 = ( 𝑦 ∈ 𝐵 ↦ ( 𝑆 × { 𝑦 } ) )
12	10 11	fnmpti	⊢ ◡ 𝐹 Fn 𝐵
13		dff1o4	⊢ ( 𝐹 : ( 𝐵 ↑m 𝑆 ) –1-1-onto→ 𝐵 ↔ ( 𝐹 Fn ( 𝐵 ↑m 𝑆 ) ∧ ◡ 𝐹 Fn 𝐵 ) )
14	6 12 13	mpbir2an	⊢ 𝐹 : ( 𝐵 ↑m 𝑆 ) –1-1-onto→ 𝐵