Metamath Proof Explorer


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 )