Theorem opoc1

Description: Orthocomplement of orthoposet unity. (Contributed by NM, 24-Jan-2012)

	Ref	Expression
Hypotheses	opoc1.z	|- .0. = ( 0. ` K )
	opoc1.u	|- .1. = ( 1. ` K )
	opoc1.o	|- ._|_ = ( oc ` K )
Assertion	opoc1	|- ( K e. OP -> ( ._|_ ` .1. ) = .0. )

Proof

Step	Hyp	Ref	Expression
1		opoc1.z	|- .0. = ( 0. ` K )
2		opoc1.u	|- .1. = ( 1. ` K )
3		opoc1.o	|- ._|_ = ( oc ` K )
4		eqid	|- ( Base ` K ) = ( Base ` K )
5	4 1	op0cl	|- ( K e. OP -> .0. e. ( Base ` K ) )
6	4 3	opoccl	|- ( ( K e. OP /\ .0. e. ( Base ` K ) ) -> ( ._|_ ` .0. ) e. ( Base ` K ) )
7	5 6	mpdan	|- ( K e. OP -> ( ._|_ ` .0. ) e. ( Base ` K ) )
8		eqid	|- ( le ` K ) = ( le ` K )
9	4 8 2	ople1	|- ( ( K e. OP /\ ( ._|_ ` .0. ) e. ( Base ` K ) ) -> ( ._|_ ` .0. ) ( le ` K ) .1. )
10	7 9	mpdan	|- ( K e. OP -> ( ._|_ ` .0. ) ( le ` K ) .1. )
11	4 2	op1cl	|- ( K e. OP -> .1. e. ( Base ` K ) )
12	4 8 3	oplecon1b	|- ( ( K e. OP /\ .1. e. ( Base ` K ) /\ .0. e. ( Base ` K ) ) -> ( ( ._|_ ` .1. ) ( le ` K ) .0. <-> ( ._|_ ` .0. ) ( le ` K ) .1. ) )
13	11 5 12	mpd3an23	|- ( K e. OP -> ( ( ._|_ ` .1. ) ( le ` K ) .0. <-> ( ._|_ ` .0. ) ( le ` K ) .1. ) )
14	10 13	mpbird	|- ( K e. OP -> ( ._|_ ` .1. ) ( le ` K ) .0. )
15	4 3	opoccl	|- ( ( K e. OP /\ .1. e. ( Base ` K ) ) -> ( ._|_ ` .1. ) e. ( Base ` K ) )
16	11 15	mpdan	|- ( K e. OP -> ( ._|_ ` .1. ) e. ( Base ` K ) )
17	4 8 1	ople0	|- ( ( K e. OP /\ ( ._|_ ` .1. ) e. ( Base ` K ) ) -> ( ( ._|_ ` .1. ) ( le ` K ) .0. <-> ( ._|_ ` .1. ) = .0. ) )
18	16 17	mpdan	|- ( K e. OP -> ( ( ._|_ ` .1. ) ( le ` K ) .0. <-> ( ._|_ ` .1. ) = .0. ) )
19	14 18	mpbid	|- ( K e. OP -> ( ._|_ ` .1. ) = .0. )