Description: An orthoposet has a unit element. ( helch analog.) (Contributed by NM, 22-Oct-2011)
Ref | Expression | ||
---|---|---|---|
Hypotheses | op1cl.b | ⊢ 𝐵 = ( Base ‘ 𝐾 ) | |
op1cl.u | ⊢ 1 = ( 1. ‘ 𝐾 ) | ||
Assertion | op1cl | ⊢ ( 𝐾 ∈ OP → 1 ∈ 𝐵 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | op1cl.b | ⊢ 𝐵 = ( Base ‘ 𝐾 ) | |
2 | op1cl.u | ⊢ 1 = ( 1. ‘ 𝐾 ) | |
3 | eqid | ⊢ ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 ) | |
4 | 1 3 2 | p1val | ⊢ ( 𝐾 ∈ OP → 1 = ( ( lub ‘ 𝐾 ) ‘ 𝐵 ) ) |
5 | id | ⊢ ( 𝐾 ∈ OP → 𝐾 ∈ OP ) | |
6 | eqid | ⊢ ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 ) | |
7 | 1 3 6 | op01dm | ⊢ ( 𝐾 ∈ OP → ( 𝐵 ∈ dom ( lub ‘ 𝐾 ) ∧ 𝐵 ∈ dom ( glb ‘ 𝐾 ) ) ) |
8 | 7 | simpld | ⊢ ( 𝐾 ∈ OP → 𝐵 ∈ dom ( lub ‘ 𝐾 ) ) |
9 | 1 3 5 8 | lubcl | ⊢ ( 𝐾 ∈ OP → ( ( lub ‘ 𝐾 ) ‘ 𝐵 ) ∈ 𝐵 ) |
10 | 4 9 | eqeltrd | ⊢ ( 𝐾 ∈ OP → 1 ∈ 𝐵 ) |