Theorem opoc0

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

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

Proof

Step	Hyp	Ref	Expression
1		opoc1.z	|- .0. = ( 0. ` K )
2		opoc1.u	|- .1. = ( 1. ` K )
3		opoc1.o	|- ._|_ = ( oc ` K )
4	1 2 3	opoc1	|- ( K e. OP -> ( ._|_ ` .1. ) = .0. )
5		eqid	|- ( Base ` K ) = ( Base ` K )
6	5 2	op1cl	|- ( K e. OP -> .1. e. ( Base ` K ) )
7	5 1	op0cl	|- ( K e. OP -> .0. e. ( Base ` K ) )
8	5 3	opcon1b	|- ( ( K e. OP /\ .1. e. ( Base ` K ) /\ .0. e. ( Base ` K ) ) -> ( ( ._|_ ` .1. ) = .0. <-> ( ._|_ ` .0. ) = .1. ) )
9	6 7 8	mpd3an23	|- ( K e. OP -> ( ( ._|_ ` .1. ) = .0. <-> ( ._|_ ` .0. ) = .1. ) )
10	4 9	mpbid	|- ( K e. OP -> ( ._|_ ` .0. ) = .1. )