This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-ocomp

Description: Define the orthocomplementation extractor for posets and related structures. (Contributed by NM, 4-Sep-2011) (Revised by Mario Carneiro, 14-Aug-2015) Use its index-independent form ocid instead. (New usage is discouraged.)

		Ref	Expression
	Assertion	df-ocomp	\|- oc = Slot ; 1 1

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		coc	\|- oc
1		c1	\|- 1
2	1 1	cdc	\|- ; 1 1
3	2	cslot	\|- Slot ; 1 1
4	0 3	wceq	\|- oc = Slot ; 1 1