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 )