Step |
Hyp |
Ref |
Expression |
1 |
|
dibcl.h |
|- H = ( LHyp ` K ) |
2 |
|
dibcl.i |
|- I = ( ( DIsoB ` K ) ` W ) |
3 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
4 |
|
eqid |
|- ( le ` K ) = ( le ` K ) |
5 |
3 4 1 2
|
dibfnN |
|- ( ( K e. HL /\ W e. H ) -> I Fn { x e. ( Base ` K ) | x ( le ` K ) W } ) |
6 |
|
fnfun |
|- ( I Fn { x e. ( Base ` K ) | x ( le ` K ) W } -> Fun I ) |
7 |
|
funfn |
|- ( Fun I <-> I Fn dom I ) |
8 |
6 7
|
sylib |
|- ( I Fn { x e. ( Base ` K ) | x ( le ` K ) W } -> I Fn dom I ) |
9 |
5 8
|
syl |
|- ( ( K e. HL /\ W e. H ) -> I Fn dom I ) |
10 |
|
eqidd |
|- ( ( K e. HL /\ W e. H ) -> ran I = ran I ) |
11 |
3 4 1 2
|
dibeldmN |
|- ( ( K e. HL /\ W e. H ) -> ( x e. dom I <-> ( x e. ( Base ` K ) /\ x ( le ` K ) W ) ) ) |
12 |
3 4 1 2
|
dibeldmN |
|- ( ( K e. HL /\ W e. H ) -> ( y e. dom I <-> ( y e. ( Base ` K ) /\ y ( le ` K ) W ) ) ) |
13 |
11 12
|
anbi12d |
|- ( ( K e. HL /\ W e. H ) -> ( ( x e. dom I /\ y e. dom I ) <-> ( ( x e. ( Base ` K ) /\ x ( le ` K ) W ) /\ ( y e. ( Base ` K ) /\ y ( le ` K ) W ) ) ) ) |
14 |
3 4 1 2
|
dib11N |
|- ( ( ( K e. HL /\ W e. H ) /\ ( x e. ( Base ` K ) /\ x ( le ` K ) W ) /\ ( y e. ( Base ` K ) /\ y ( le ` K ) W ) ) -> ( ( I ` x ) = ( I ` y ) <-> x = y ) ) |
15 |
14
|
biimpd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( x e. ( Base ` K ) /\ x ( le ` K ) W ) /\ ( y e. ( Base ` K ) /\ y ( le ` K ) W ) ) -> ( ( I ` x ) = ( I ` y ) -> x = y ) ) |
16 |
15
|
3expib |
|- ( ( K e. HL /\ W e. H ) -> ( ( ( x e. ( Base ` K ) /\ x ( le ` K ) W ) /\ ( y e. ( Base ` K ) /\ y ( le ` K ) W ) ) -> ( ( I ` x ) = ( I ` y ) -> x = y ) ) ) |
17 |
13 16
|
sylbid |
|- ( ( K e. HL /\ W e. H ) -> ( ( x e. dom I /\ y e. dom I ) -> ( ( I ` x ) = ( I ` y ) -> x = y ) ) ) |
18 |
17
|
ralrimivv |
|- ( ( K e. HL /\ W e. H ) -> A. x e. dom I A. y e. dom I ( ( I ` x ) = ( I ` y ) -> x = y ) ) |
19 |
|
dff1o6 |
|- ( I : dom I -1-1-onto-> ran I <-> ( I Fn dom I /\ ran I = ran I /\ A. x e. dom I A. y e. dom I ( ( I ` x ) = ( I ` y ) -> x = y ) ) ) |
20 |
9 10 18 19
|
syl3anbrc |
|- ( ( K e. HL /\ W e. H ) -> I : dom I -1-1-onto-> ran I ) |