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 
|- S = { X }
mapsncnv.b 
|- B e. _V
mapsncnv.x 
|- X e. _V
mapsnf1o3.f 
|- F = ( y e. B |-> ( S X. { y } ) )
Assertion mapsnf1o3 
|- F : B -1-1-onto-> ( B ^m S )

Proof

Step Hyp Ref Expression
1 mapsncnv.s 
 |-  S = { X }
2 mapsncnv.b 
 |-  B e. _V
3 mapsncnv.x 
 |-  X e. _V
4 mapsnf1o3.f 
 |-  F = ( y e. B |-> ( S X. { y } ) )
5 eqid 
 |-  ( x e. ( B ^m S ) |-> ( x ` X ) ) = ( x e. ( B ^m S ) |-> ( x ` X ) )
6 1 2 3 5 mapsnf1o2 
 |-  ( x e. ( B ^m S ) |-> ( x ` X ) ) : ( B ^m S ) -1-1-onto-> B
7 f1ocnv 
 |-  ( ( x e. ( B ^m S ) |-> ( x ` X ) ) : ( B ^m S ) -1-1-onto-> B -> `' ( x e. ( B ^m S ) |-> ( x ` X ) ) : B -1-1-onto-> ( B ^m S ) )
8 6 7 ax-mp 
 |-  `' ( x e. ( B ^m S ) |-> ( x ` X ) ) : B -1-1-onto-> ( B ^m S )
9 1 2 3 5 mapsncnv 
 |-  `' ( x e. ( B ^m S ) |-> ( x ` X ) ) = ( y e. B |-> ( S X. { y } ) )
10 4 9 eqtr4i 
 |-  F = `' ( x e. ( B ^m S ) |-> ( x ` X ) )
11 f1oeq1 
 |-  ( F = `' ( x e. ( B ^m S ) |-> ( x ` X ) ) -> ( F : B -1-1-onto-> ( B ^m S ) <-> `' ( x e. ( B ^m S ) |-> ( x ` X ) ) : B -1-1-onto-> ( B ^m S ) ) )
12 10 11 ax-mp 
 |-  ( F : B -1-1-onto-> ( B ^m S ) <-> `' ( x e. ( B ^m S ) |-> ( x ` X ) ) : B -1-1-onto-> ( B ^m S ) )
13 8 12 mpbir 
 |-  F : B -1-1-onto-> ( B ^m S )