Step |
Hyp |
Ref |
Expression |
1 |
|
adj1o |
|- adjh : dom adjh -1-1-onto-> dom adjh |
2 |
|
f1of1 |
|- ( adjh : dom adjh -1-1-onto-> dom adjh -> adjh : dom adjh -1-1-> dom adjh ) |
3 |
1 2
|
ax-mp |
|- adjh : dom adjh -1-1-> dom adjh |
4 |
|
bdopssadj |
|- BndLinOp C_ dom adjh |
5 |
|
f1ores |
|- ( ( adjh : dom adjh -1-1-> dom adjh /\ BndLinOp C_ dom adjh ) -> ( adjh |` BndLinOp ) : BndLinOp -1-1-onto-> ( adjh " BndLinOp ) ) |
6 |
3 4 5
|
mp2an |
|- ( adjh |` BndLinOp ) : BndLinOp -1-1-onto-> ( adjh " BndLinOp ) |
7 |
|
vex |
|- y e. _V |
8 |
7
|
elima |
|- ( y e. ( adjh " BndLinOp ) <-> E. x e. BndLinOp x adjh y ) |
9 |
|
f1ofn |
|- ( adjh : dom adjh -1-1-onto-> dom adjh -> adjh Fn dom adjh ) |
10 |
1 9
|
ax-mp |
|- adjh Fn dom adjh |
11 |
|
bdopadj |
|- ( x e. BndLinOp -> x e. dom adjh ) |
12 |
|
fnbrfvb |
|- ( ( adjh Fn dom adjh /\ x e. dom adjh ) -> ( ( adjh ` x ) = y <-> x adjh y ) ) |
13 |
10 11 12
|
sylancr |
|- ( x e. BndLinOp -> ( ( adjh ` x ) = y <-> x adjh y ) ) |
14 |
13
|
rexbiia |
|- ( E. x e. BndLinOp ( adjh ` x ) = y <-> E. x e. BndLinOp x adjh y ) |
15 |
|
adjbdlnb |
|- ( x e. BndLinOp <-> ( adjh ` x ) e. BndLinOp ) |
16 |
|
eleq1 |
|- ( ( adjh ` x ) = y -> ( ( adjh ` x ) e. BndLinOp <-> y e. BndLinOp ) ) |
17 |
15 16
|
syl5bb |
|- ( ( adjh ` x ) = y -> ( x e. BndLinOp <-> y e. BndLinOp ) ) |
18 |
17
|
biimpcd |
|- ( x e. BndLinOp -> ( ( adjh ` x ) = y -> y e. BndLinOp ) ) |
19 |
18
|
rexlimiv |
|- ( E. x e. BndLinOp ( adjh ` x ) = y -> y e. BndLinOp ) |
20 |
|
adjbdln |
|- ( y e. BndLinOp -> ( adjh ` y ) e. BndLinOp ) |
21 |
|
bdopadj |
|- ( y e. BndLinOp -> y e. dom adjh ) |
22 |
|
adjadj |
|- ( y e. dom adjh -> ( adjh ` ( adjh ` y ) ) = y ) |
23 |
21 22
|
syl |
|- ( y e. BndLinOp -> ( adjh ` ( adjh ` y ) ) = y ) |
24 |
|
fveqeq2 |
|- ( x = ( adjh ` y ) -> ( ( adjh ` x ) = y <-> ( adjh ` ( adjh ` y ) ) = y ) ) |
25 |
24
|
rspcev |
|- ( ( ( adjh ` y ) e. BndLinOp /\ ( adjh ` ( adjh ` y ) ) = y ) -> E. x e. BndLinOp ( adjh ` x ) = y ) |
26 |
20 23 25
|
syl2anc |
|- ( y e. BndLinOp -> E. x e. BndLinOp ( adjh ` x ) = y ) |
27 |
19 26
|
impbii |
|- ( E. x e. BndLinOp ( adjh ` x ) = y <-> y e. BndLinOp ) |
28 |
8 14 27
|
3bitr2i |
|- ( y e. ( adjh " BndLinOp ) <-> y e. BndLinOp ) |
29 |
28
|
eqriv |
|- ( adjh " BndLinOp ) = BndLinOp |
30 |
|
f1oeq3 |
|- ( ( adjh " BndLinOp ) = BndLinOp -> ( ( adjh |` BndLinOp ) : BndLinOp -1-1-onto-> ( adjh " BndLinOp ) <-> ( adjh |` BndLinOp ) : BndLinOp -1-1-onto-> BndLinOp ) ) |
31 |
29 30
|
ax-mp |
|- ( ( adjh |` BndLinOp ) : BndLinOp -1-1-onto-> ( adjh " BndLinOp ) <-> ( adjh |` BndLinOp ) : BndLinOp -1-1-onto-> BndLinOp ) |
32 |
6 31
|
mpbi |
|- ( adjh |` BndLinOp ) : BndLinOp -1-1-onto-> BndLinOp |