Theorem opoc1

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

	Ref	Expression
Hypotheses	opoc1.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
	opoc1.u	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
	opoc1.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$
Assertion	opoc1	$$⊢K\in \mathrm{OP}\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{1}\right)=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		opoc1.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
2		opoc1.u	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
3		opoc1.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$
4		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
5	4 1	op0cl	$$⊢K\in \mathrm{OP}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_K$$
6	4 3	opoccl	$$⊢\left(K\in \mathrm{OP}\wedge \underset{\dot{}}{0}\in {\mathrm{Base}}_K\right)\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_K$$
7	5 6	mpdan	$$⊢K\in \mathrm{OP}\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_K$$
8		eqid	$$⊢{\le }_K={\le }_K$$
9	4 8 2	ople1	$$⊢\left(K\in \mathrm{OP}\wedge \underset{\dot{}}{\perp }\left(\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_K\right)\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{0}\right){\le }_K\underset{\dot{}}{1}$$
10	7 9	mpdan	$$⊢K\in \mathrm{OP}\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{0}\right){\le }_K\underset{\dot{}}{1}$$
11	4 2	op1cl	$$⊢K\in \mathrm{OP}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_K$$
12	4 8 3	oplecon1b	$$⊢\left(K\in \mathrm{OP}\wedge \underset{\dot{}}{1}\in {\mathrm{Base}}_K\wedge \underset{\dot{}}{0}\in {\mathrm{Base}}_K\right)\to \left(\underset{\dot{}}{\perp }\left(\underset{\dot{}}{1}\right){\le }_K\underset{\dot{}}{0}\leftrightarrow \underset{\dot{}}{\perp }\left(\underset{\dot{}}{0}\right){\le }_K\underset{\dot{}}{1}\right)$$
13	11 5 12	mpd3an23	$$⊢K\in \mathrm{OP}\to \left(\underset{\dot{}}{\perp }\left(\underset{\dot{}}{1}\right){\le }_K\underset{\dot{}}{0}\leftrightarrow \underset{\dot{}}{\perp }\left(\underset{\dot{}}{0}\right){\le }_K\underset{\dot{}}{1}\right)$$
14	10 13	mpbird	$$⊢K\in \mathrm{OP}\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{1}\right){\le }_K\underset{\dot{}}{0}$$
15	4 3	opoccl	$$⊢\left(K\in \mathrm{OP}\wedge \underset{\dot{}}{1}\in {\mathrm{Base}}_K\right)\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{1}\right)\in {\mathrm{Base}}_K$$
16	11 15	mpdan	$$⊢K\in \mathrm{OP}\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{1}\right)\in {\mathrm{Base}}_K$$
17	4 8 1	ople0	$$⊢\left(K\in \mathrm{OP}\wedge \underset{\dot{}}{\perp }\left(\underset{\dot{}}{1}\right)\in {\mathrm{Base}}_K\right)\to \left(\underset{\dot{}}{\perp }\left(\underset{\dot{}}{1}\right){\le }_K\underset{\dot{}}{0}\leftrightarrow \underset{\dot{}}{\perp }\left(\underset{\dot{}}{1}\right)=\underset{\dot{}}{0}\right)$$
18	16 17	mpdan	$$⊢K\in \mathrm{OP}\to \left(\underset{\dot{}}{\perp }\left(\underset{\dot{}}{1}\right){\le }_K\underset{\dot{}}{0}\leftrightarrow \underset{\dot{}}{\perp }\left(\underset{\dot{}}{1}\right)=\underset{\dot{}}{0}\right)$$
19	14 18	mpbid	$$⊢K\in \mathrm{OP}\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{1}\right)=\underset{\dot{}}{0}$$