opoc0

Description: Orthocomplement of orthoposet zero. (Contributed by NM, 24-Jan-2012)

	Ref	Expression
Hypotheses	opoc1.z	$⊢ \underset{˙}{0} = 0. (K)$
	opoc1.u	$⊢ \underset{˙}{1} = 1. (K)$
	opoc1.o	$⊢ \underset{˙}{⊥} = oc (K)$
Assertion	opoc0	$⊢ K \in OP \to \underset{˙}{⊥} (\underset{˙}{0}) = \underset{˙}{1}$

Step	Hyp	Ref	Expression
1		opoc1.z	$⊢ \underset{˙}{0} = 0. (K)$
2		opoc1.u	$⊢ \underset{˙}{1} = 1. (K)$
3		opoc1.o	$⊢ \underset{˙}{⊥} = oc (K)$
4	1 2 3	opoc1	$⊢ K \in OP \to \underset{˙}{⊥} (\underset{˙}{1}) = \underset{˙}{0}$
5		eqid	$⊢ {Base}_{K} = {Base}_{K}$
6	5 2	op1cl	$⊢ K \in OP \to \underset{˙}{1} \in {Base}_{K}$
7	5 1	op0cl	$⊢ K \in OP \to \underset{˙}{0} \in {Base}_{K}$
8	5 3	opcon1b	$⊢ (K \in OP \land \underset{˙}{1} \in {Base}_{K} \land \underset{˙}{0} \in {Base}_{K}) \to (\underset{˙}{⊥} (\underset{˙}{1}) = \underset{˙}{0} \leftrightarrow \underset{˙}{⊥} (\underset{˙}{0}) = \underset{˙}{1})$
9	6 7 8	mpd3an23	$⊢ K \in OP \to (\underset{˙}{⊥} (\underset{˙}{1}) = \underset{˙}{0} \leftrightarrow \underset{˙}{⊥} (\underset{˙}{0}) = \underset{˙}{1})$
10	4 9	mpbid	$⊢ K \in OP \to \underset{˙}{⊥} (\underset{˙}{0}) = \underset{˙}{1}$

Metamath Proof Explorer