Theorem oplecon3

Description: Contraposition law for orthoposets. (Contributed by NM, 13-Sep-2011)

	Ref	Expression
Hypotheses	opcon3.b	$$⊢B={\mathrm{Base}}_K$$
	opcon3.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	opcon3.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$
Assertion	oplecon3	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{\le }Y\to \underset{\dot{}}{\perp }\left(Y\right)\underset{\dot{}}{\le }\underset{\dot{}}{\perp }\left(X\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		opcon3.b	$$⊢B={\mathrm{Base}}_K$$
2		opcon3.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		opcon3.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$
4		eqid	$$⊢\mathrm{join}\left(K\right)=\mathrm{join}\left(K\right)$$
5		eqid	$$⊢\mathrm{meet}\left(K\right)=\mathrm{meet}\left(K\right)$$
6		eqid	$$⊢\mathrm{0.}\left(K\right)=\mathrm{0.}\left(K\right)$$
7		eqid	$$⊢\mathrm{1.}\left(K\right)=\mathrm{1.}\left(K\right)$$
8	1 2 3 4 5 6 7	oposlem	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\wedge Y\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\underset{\dot{}}{\le }Y\to \underset{\dot{}}{\perp }\left(Y\right)\underset{\dot{}}{\le }\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\mathrm{meet}\left(K\right)\underset{\dot{}}{\perp }\left(X\right)=\mathrm{0.}\left(K\right)\right)$$
9	8	simp1d	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\wedge Y\in B\right)\to \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\underset{\dot{}}{\le }Y\to \underset{\dot{}}{\perp }\left(Y\right)\underset{\dot{}}{\le }\underset{\dot{}}{\perp }\left(X\right)\right)\right)$$
10	9	simp3d	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{\le }Y\to \underset{\dot{}}{\perp }\left(Y\right)\underset{\dot{}}{\le }\underset{\dot{}}{\perp }\left(X\right)\right)$$