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 ) |