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

Metamath Proof Explorer

Theorem pwssnf1o

Description: Triviality of singleton powers: set equipollence. (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Hypotheses pwssnf1o.y 
|- Y = ( R ^s { I } )
pwssnf1o.b 
|- B = ( Base ` R )
pwssnf1o.f 
|- F = ( x e. B |-> ( { I } X. { x } ) )
pwssnf1o.c 
|- C = ( Base ` Y )
Assertion pwssnf1o 
|- ( ( R e. V /\ I e. W ) -> F : B -1-1-onto-> C )

Proof

Step Hyp Ref Expression
1 pwssnf1o.y 
 |-  Y = ( R ^s { I } )
2 pwssnf1o.b 
 |-  B = ( Base ` R )
3 pwssnf1o.f 
 |-  F = ( x e. B |-> ( { I } X. { x } ) )
4 pwssnf1o.c 
 |-  C = ( Base ` Y )
5 2 fvexi 
 |-  B e. _V
6 simpr 
 |-  ( ( R e. V /\ I e. W ) -> I e. W )
7 3 mapsnf1o 
 |-  ( ( B e. _V /\ I e. W ) -> F : B -1-1-onto-> ( B ^m { I } ) )
8 5 6 7 sylancr 
 |-  ( ( R e. V /\ I e. W ) -> F : B -1-1-onto-> ( B ^m { I } ) )
9 snex 
 |-  { I } e. _V
10 1 2 pwsbas 
 |-  ( ( R e. V /\ { I } e. _V ) -> ( B ^m { I } ) = ( Base ` Y ) )
11 9 10 mpan2 
 |-  ( R e. V -> ( B ^m { I } ) = ( Base ` Y ) )
12 11 adantr 
 |-  ( ( R e. V /\ I e. W ) -> ( B ^m { I } ) = ( Base ` Y ) )
13 4 12 eqtr4id 
 |-  ( ( R e. V /\ I e. W ) -> C = ( B ^m { I } ) )
14 13 f1oeq3d 
 |-  ( ( R e. V /\ I e. W ) -> ( F : B -1-1-onto-> C <-> F : B -1-1-onto-> ( B ^m { I } ) ) )
15 8 14 mpbird 
 |-  ( ( R e. V /\ I e. W ) -> F : B -1-1-onto-> C )