Step |
Hyp |
Ref |
Expression |
1 |
|
opoccl.b |
|- B = ( Base ` K ) |
2 |
|
opoccl.o |
|- ._|_ = ( oc ` K ) |
3 |
|
fveq2 |
|- ( Y = X -> ( ._|_ ` Y ) = ( ._|_ ` X ) ) |
4 |
3
|
eqcoms |
|- ( X = Y -> ( ._|_ ` Y ) = ( ._|_ ` X ) ) |
5 |
|
fveq2 |
|- ( ( ._|_ ` X ) = ( ._|_ ` Y ) -> ( ._|_ ` ( ._|_ ` X ) ) = ( ._|_ ` ( ._|_ ` Y ) ) ) |
6 |
5
|
eqcoms |
|- ( ( ._|_ ` Y ) = ( ._|_ ` X ) -> ( ._|_ ` ( ._|_ ` X ) ) = ( ._|_ ` ( ._|_ ` Y ) ) ) |
7 |
1 2
|
opococ |
|- ( ( K e. OP /\ X e. B ) -> ( ._|_ ` ( ._|_ ` X ) ) = X ) |
8 |
7
|
3adant3 |
|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( ._|_ ` X ) ) = X ) |
9 |
1 2
|
opococ |
|- ( ( K e. OP /\ Y e. B ) -> ( ._|_ ` ( ._|_ ` Y ) ) = Y ) |
10 |
9
|
3adant2 |
|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( ._|_ ` Y ) ) = Y ) |
11 |
8 10
|
eqeq12d |
|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` ( ._|_ ` X ) ) = ( ._|_ ` ( ._|_ ` Y ) ) <-> X = Y ) ) |
12 |
6 11
|
syl5ib |
|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` Y ) = ( ._|_ ` X ) -> X = Y ) ) |
13 |
4 12
|
impbid2 |
|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( X = Y <-> ( ._|_ ` Y ) = ( ._|_ ` X ) ) ) |