Theorem opoc0

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

	Ref	Expression
Hypotheses	opoc1.z	⊢ 0 = ( 0. ‘ 𝐾 )
	opoc1.u	⊢ 1 = ( 1. ‘ 𝐾 )
	opoc1.o	⊢ ⊥ = ( oc ‘ 𝐾 )
Assertion	opoc0	⊢ ( 𝐾 ∈ OP → ( ⊥ ‘ 0 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		opoc1.z	⊢ 0 = ( 0. ‘ 𝐾 )
2		opoc1.u	⊢ 1 = ( 1. ‘ 𝐾 )
3		opoc1.o	⊢ ⊥ = ( oc ‘ 𝐾 )
4	1 2 3	opoc1	⊢ ( 𝐾 ∈ OP → ( ⊥ ‘ 1 ) = 0 )
5		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
6	5 2	op1cl	⊢ ( 𝐾 ∈ OP → 1 ∈ ( Base ‘ 𝐾 ) )
7	5 1	op0cl	⊢ ( 𝐾 ∈ OP → 0 ∈ ( Base ‘ 𝐾 ) )
8	5 3	opcon1b	⊢ ( ( 𝐾 ∈ OP ∧ 1 ∈ ( Base ‘ 𝐾 ) ∧ 0 ∈ ( Base ‘ 𝐾 ) ) → ( ( ⊥ ‘ 1 ) = 0 ↔ ( ⊥ ‘ 0 ) = 1 ) )
9	6 7 8	mpd3an23	⊢ ( 𝐾 ∈ OP → ( ( ⊥ ‘ 1 ) = 0 ↔ ( ⊥ ‘ 0 ) = 1 ) )
10	4 9	mpbid	⊢ ( 𝐾 ∈ OP → ( ⊥ ‘ 0 ) = 1 )