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

Metamath Proof Explorer

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 )