Theorem opoc1

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

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

Proof

Step	Hyp	Ref	Expression
1		opoc1.z	⊢ 0 = ( 0. ‘ 𝐾 )
2		opoc1.u	⊢ 1 = ( 1. ‘ 𝐾 )
3		opoc1.o	⊢ ⊥ = ( oc ‘ 𝐾 )
4		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
5	4 1	op0cl	⊢ ( 𝐾 ∈ OP → 0 ∈ ( Base ‘ 𝐾 ) )
6	4 3	opoccl	⊢ ( ( 𝐾 ∈ OP ∧ 0 ∈ ( Base ‘ 𝐾 ) ) → ( ⊥ ‘ 0 ) ∈ ( Base ‘ 𝐾 ) )
7	5 6	mpdan	⊢ ( 𝐾 ∈ OP → ( ⊥ ‘ 0 ) ∈ ( Base ‘ 𝐾 ) )
8		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
9	4 8 2	ople1	⊢ ( ( 𝐾 ∈ OP ∧ ( ⊥ ‘ 0 ) ∈ ( Base ‘ 𝐾 ) ) → ( ⊥ ‘ 0 ) ( le ‘ 𝐾 ) 1 )
10	7 9	mpdan	⊢ ( 𝐾 ∈ OP → ( ⊥ ‘ 0 ) ( le ‘ 𝐾 ) 1 )
11	4 2	op1cl	⊢ ( 𝐾 ∈ OP → 1 ∈ ( Base ‘ 𝐾 ) )
12	4 8 3	oplecon1b	⊢ ( ( 𝐾 ∈ OP ∧ 1 ∈ ( Base ‘ 𝐾 ) ∧ 0 ∈ ( Base ‘ 𝐾 ) ) → ( ( ⊥ ‘ 1 ) ( le ‘ 𝐾 ) 0 ↔ ( ⊥ ‘ 0 ) ( le ‘ 𝐾 ) 1 ) )
13	11 5 12	mpd3an23	⊢ ( 𝐾 ∈ OP → ( ( ⊥ ‘ 1 ) ( le ‘ 𝐾 ) 0 ↔ ( ⊥ ‘ 0 ) ( le ‘ 𝐾 ) 1 ) )
14	10 13	mpbird	⊢ ( 𝐾 ∈ OP → ( ⊥ ‘ 1 ) ( le ‘ 𝐾 ) 0 )
15	4 3	opoccl	⊢ ( ( 𝐾 ∈ OP ∧ 1 ∈ ( Base ‘ 𝐾 ) ) → ( ⊥ ‘ 1 ) ∈ ( Base ‘ 𝐾 ) )
16	11 15	mpdan	⊢ ( 𝐾 ∈ OP → ( ⊥ ‘ 1 ) ∈ ( Base ‘ 𝐾 ) )
17	4 8 1	ople0	⊢ ( ( 𝐾 ∈ OP ∧ ( ⊥ ‘ 1 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( ⊥ ‘ 1 ) ( le ‘ 𝐾 ) 0 ↔ ( ⊥ ‘ 1 ) = 0 ) )
18	16 17	mpdan	⊢ ( 𝐾 ∈ OP → ( ( ⊥ ‘ 1 ) ( le ‘ 𝐾 ) 0 ↔ ( ⊥ ‘ 1 ) = 0 ) )
19	14 18	mpbid	⊢ ( 𝐾 ∈ OP → ( ⊥ ‘ 1 ) = 0 )