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

Metamath Proof Explorer

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 𝑆 )