Theorem f1opw

Description: A one-to-one mapping induces a one-to-one mapping on power sets. (Contributed by Stefan O'Rear, 18-Nov-2014) (Revised by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Assertion	f1opw	|- ( F : A -1-1-onto-> B -> ( b e. ~P A |-> ( F " b ) ) : ~P A -1-1-onto-> ~P B )

Proof

Step	Hyp	Ref	Expression
1		id	|- ( F : A -1-1-onto-> B -> F : A -1-1-onto-> B )
2		dff1o3	|- ( F : A -1-1-onto-> B <-> ( F : A -onto-> B /\ Fun `' F ) )
3		vex	|- a e. _V
4	3	funimaex	|- ( Fun `' F -> ( `' F " a ) e. _V )
5	2 4	simplbiim	|- ( F : A -1-1-onto-> B -> ( `' F " a ) e. _V )
6		f1ofun	|- ( F : A -1-1-onto-> B -> Fun F )
7		vex	|- b e. _V
8	7	funimaex	|- ( Fun F -> ( F " b ) e. _V )
9	6 8	syl	|- ( F : A -1-1-onto-> B -> ( F " b ) e. _V )
10	1 5 9	f1opw2	|- ( F : A -1-1-onto-> B -> ( b e. ~P A |-> ( F " b ) ) : ~P A -1-1-onto-> ~P B )