Theorem opcon1b

Description: Orthocomplement contraposition law. ( negcon1 analog.) (Contributed by NM, 24-Jan-2012)

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

Proof

Step	Hyp	Ref	Expression
1		opoccl.b	$$⊢B={\mathrm{Base}}_K$$
2		opoccl.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$
3	1 2	opcon2b	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\wedge Y\in B\right)\to \left(X=\underset{\dot{}}{\perp }\left(Y\right)\leftrightarrow Y=\underset{\dot{}}{\perp }\left(X\right)\right)$$
4		eqcom	$$⊢\underset{\dot{}}{\perp }\left(Y\right)=X\leftrightarrow X=\underset{\dot{}}{\perp }\left(Y\right)$$
5		eqcom	$$⊢\underset{\dot{}}{\perp }\left(X\right)=Y\leftrightarrow Y=\underset{\dot{}}{\perp }\left(X\right)$$
6	3 4 5	3bitr4g	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\wedge Y\in B\right)\to \left(\underset{\dot{}}{\perp }\left(Y\right)=X\leftrightarrow \underset{\dot{}}{\perp }\left(X\right)=Y\right)$$
7	6	bicomd	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\wedge Y\in B\right)\to \left(\underset{\dot{}}{\perp }\left(X\right)=Y\leftrightarrow \underset{\dot{}}{\perp }\left(Y\right)=X\right)$$