Theorem mapsnf1o3

Description: Explicit bijection in the reverse of mapsnf1o2 . (Contributed by Stefan O'Rear, 24-Mar-2015)

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

Proof

Step	Hyp	Ref	Expression
1		mapsncnv.s	⊢ 𝑆 = { 𝑋 }
2		mapsncnv.b	⊢ 𝐵 ∈ V
3		mapsncnv.x	⊢ 𝑋 ∈ V
4		mapsnf1o3.f	⊢ 𝐹 = ( 𝑦 ∈ 𝐵 ↦ ( 𝑆 × { 𝑦 } ) )
5		eqid	⊢ ( 𝑥 ∈ ( 𝐵 ↑m 𝑆 ) ↦ ( 𝑥 ‘ 𝑋 ) ) = ( 𝑥 ∈ ( 𝐵 ↑m 𝑆 ) ↦ ( 𝑥 ‘ 𝑋 ) )
6	1 2 3 5	mapsnf1o2	⊢ ( 𝑥 ∈ ( 𝐵 ↑m 𝑆 ) ↦ ( 𝑥 ‘ 𝑋 ) ) : ( 𝐵 ↑m 𝑆 ) –1-1-onto→ 𝐵
7		f1ocnv	⊢ ( ( 𝑥 ∈ ( 𝐵 ↑m 𝑆 ) ↦ ( 𝑥 ‘ 𝑋 ) ) : ( 𝐵 ↑m 𝑆 ) –1-1-onto→ 𝐵 → ◡ ( 𝑥 ∈ ( 𝐵 ↑m 𝑆 ) ↦ ( 𝑥 ‘ 𝑋 ) ) : 𝐵 –1-1-onto→ ( 𝐵 ↑m 𝑆 ) )
8	6 7	ax-mp	⊢ ◡ ( 𝑥 ∈ ( 𝐵 ↑m 𝑆 ) ↦ ( 𝑥 ‘ 𝑋 ) ) : 𝐵 –1-1-onto→ ( 𝐵 ↑m 𝑆 )
9	1 2 3 5	mapsncnv	⊢ ◡ ( 𝑥 ∈ ( 𝐵 ↑m 𝑆 ) ↦ ( 𝑥 ‘ 𝑋 ) ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝑆 × { 𝑦 } ) )
10	4 9	eqtr4i	⊢ 𝐹 = ◡ ( 𝑥 ∈ ( 𝐵 ↑m 𝑆 ) ↦ ( 𝑥 ‘ 𝑋 ) )
11		f1oeq1	⊢ ( 𝐹 = ◡ ( 𝑥 ∈ ( 𝐵 ↑m 𝑆 ) ↦ ( 𝑥 ‘ 𝑋 ) ) → ( 𝐹 : 𝐵 –1-1-onto→ ( 𝐵 ↑m 𝑆 ) ↔ ◡ ( 𝑥 ∈ ( 𝐵 ↑m 𝑆 ) ↦ ( 𝑥 ‘ 𝑋 ) ) : 𝐵 –1-1-onto→ ( 𝐵 ↑m 𝑆 ) ) )
12	10 11	ax-mp	⊢ ( 𝐹 : 𝐵 –1-1-onto→ ( 𝐵 ↑m 𝑆 ) ↔ ◡ ( 𝑥 ∈ ( 𝐵 ↑m 𝑆 ) ↦ ( 𝑥 ‘ 𝑋 ) ) : 𝐵 –1-1-onto→ ( 𝐵 ↑m 𝑆 ) )
13	8 12	mpbir	⊢ 𝐹 : 𝐵 –1-1-onto→ ( 𝐵 ↑m 𝑆 )