Theorem mapsnf1o

Description: A bijection between a set and single-point functions to it. (Contributed by Stefan O'Rear, 24-Jan-2015)

	Ref	Expression
Hypothesis	ixpsnf1o.f	|- F = ( x e. A |-> ( { I } X. { x } ) )
Assertion	mapsnf1o	|- ( ( A e. V /\ I e. W ) -> F : A -1-1-onto-> ( A ^m { I } ) )

Proof

Step	Hyp	Ref	Expression
1		ixpsnf1o.f	|- F = ( x e. A |-> ( { I } X. { x } ) )
2	1	ixpsnf1o	|- ( I e. W -> F : A -1-1-onto-> X_ y e. { I } A )
3	2	adantl	|- ( ( A e. V /\ I e. W ) -> F : A -1-1-onto-> X_ y e. { I } A )
4		snex	|- { I } e. _V
5		ixpconstg	|- ( ( { I } e. _V /\ A e. V ) -> X_ y e. { I } A = ( A ^m { I } ) )
6	5	eqcomd	|- ( ( { I } e. _V /\ A e. V ) -> ( A ^m { I } ) = X_ y e. { I } A )
7	4 6	mpan	|- ( A e. V -> ( A ^m { I } ) = X_ y e. { I } A )
8	7	adantr	|- ( ( A e. V /\ I e. W ) -> ( A ^m { I } ) = X_ y e. { I } A )
9	8	f1oeq3d	|- ( ( A e. V /\ I e. W ) -> ( F : A -1-1-onto-> ( A ^m { I } ) <-> F : A -1-1-onto-> X_ y e. { I } A ) )
10	3 9	mpbird	|- ( ( A e. V /\ I e. W ) -> F : A -1-1-onto-> ( A ^m { I } ) )