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

Metamath Proof Explorer

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