Theorem opnoncon

Description: Law of contradiction for orthoposets. ( chocin analog.) (Contributed by NM, 13-Sep-2011)

	Ref	Expression
Hypotheses	opnoncon.b	$$⊢B={\mathrm{Base}}_K$$
	opnoncon.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$
	opnoncon.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	opnoncon.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
Assertion	opnoncon	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\right)\to X\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(X\right)=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		opnoncon.b	$$⊢B={\mathrm{Base}}_K$$
2		opnoncon.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$
3		opnoncon.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
4		opnoncon.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
5		eqid	$$⊢{\le }_K={\le }_K$$
6		eqid	$$⊢\mathrm{join}\left(K\right)=\mathrm{join}\left(K\right)$$
7		eqid	$$⊢\mathrm{1.}\left(K\right)=\mathrm{1.}\left(K\right)$$
8	1 5 2 6 3 4 7	oposlem	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\wedge X\in B\right)\to \left(\left(\underset{\dot{}}{\perp }\left(X\right)\in B\wedge \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\right)\right)=X\wedge \left(X{\le }_{K}X\to \underset{\dot{}}{\perp }\left(X\right){\le }_K\underset{\dot{}}{\perp }\left(X\right)\right)\right)\wedge X\mathrm{join}\left(K\right)\underset{\dot{}}{\perp }\left(X\right)=\mathrm{1.}\left(K\right)\wedge X\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(X\right)=\underset{\dot{}}{0}\right)$$
9	8	3anidm23	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\right)\to \left(\left(\underset{\dot{}}{\perp }\left(X\right)\in B\wedge \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\right)\right)=X\wedge \left(X{\le }_{K}X\to \underset{\dot{}}{\perp }\left(X\right){\le }_K\underset{\dot{}}{\perp }\left(X\right)\right)\right)\wedge X\mathrm{join}\left(K\right)\underset{\dot{}}{\perp }\left(X\right)=\mathrm{1.}\left(K\right)\wedge X\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(X\right)=\underset{\dot{}}{0}\right)$$
10	9	simp3d	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\right)\to X\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(X\right)=\underset{\dot{}}{0}$$