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 )