Step |
Hyp |
Ref |
Expression |
1 |
|
cmt2.b |
|- B = ( Base ` K ) |
2 |
|
cmt2.o |
|- ._|_ = ( oc ` K ) |
3 |
|
cmt2.c |
|- C = ( cm ` K ) |
4 |
1 2 3
|
cmt2N |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X C Y <-> X C ( ._|_ ` Y ) ) ) |
5 |
|
omlop |
|- ( K e. OML -> K e. OP ) |
6 |
5
|
3ad2ant1 |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> K e. OP ) |
7 |
|
simp3 |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> Y e. B ) |
8 |
1 2
|
opoccl |
|- ( ( K e. OP /\ Y e. B ) -> ( ._|_ ` Y ) e. B ) |
9 |
6 7 8
|
syl2anc |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ._|_ ` Y ) e. B ) |
10 |
1 2 3
|
cmt3N |
|- ( ( K e. OML /\ X e. B /\ ( ._|_ ` Y ) e. B ) -> ( X C ( ._|_ ` Y ) <-> ( ._|_ ` X ) C ( ._|_ ` Y ) ) ) |
11 |
9 10
|
syld3an3 |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X C ( ._|_ ` Y ) <-> ( ._|_ ` X ) C ( ._|_ ` Y ) ) ) |
12 |
4 11
|
bitrd |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X C Y <-> ( ._|_ ` X ) C ( ._|_ ` Y ) ) ) |