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

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 )