Theorem opoc0

Description: Orthocomplement of orthoposet zero. (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	opoc0	$$⊢K\in \mathrm{OP}\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{1}$$

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	1 2 3	opoc1	$$⊢K\in \mathrm{OP}\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{1}\right)=\underset{\dot{}}{0}$$
5		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
6	5 2	op1cl	$$⊢K\in \mathrm{OP}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_K$$
7	5 1	op0cl	$$⊢K\in \mathrm{OP}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_K$$
8	5 3	opcon1b	$$⊢\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)=\underset{\dot{}}{0}\leftrightarrow \underset{\dot{}}{\perp }\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{1}\right)$$
9	6 7 8	mpd3an23	$$⊢K\in \mathrm{OP}\to \left(\underset{\dot{}}{\perp }\left(\underset{\dot{}}{1}\right)=\underset{\dot{}}{0}\leftrightarrow \underset{\dot{}}{\perp }\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{1}\right)$$
10	4 9	mpbid	$$⊢K\in \mathrm{OP}\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{1}$$