Description: Orthoposet zero is less than or equal to any element. ( ch0le analog.) (Contributed by NM, 12-Oct-2011)
Ref | Expression | ||
---|---|---|---|
Hypotheses | op0le.b | ⊢ 𝐵 = ( Base ‘ 𝐾 ) | |
op0le.l | ⊢ ≤ = ( le ‘ 𝐾 ) | ||
op0le.z | ⊢ 0 = ( 0. ‘ 𝐾 ) | ||
Assertion | op0le | ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → 0 ≤ 𝑋 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | op0le.b | ⊢ 𝐵 = ( Base ‘ 𝐾 ) | |
2 | op0le.l | ⊢ ≤ = ( le ‘ 𝐾 ) | |
3 | op0le.z | ⊢ 0 = ( 0. ‘ 𝐾 ) | |
4 | eqid | ⊢ ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 ) | |
5 | simpl | ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → 𝐾 ∈ OP ) | |
6 | simpr | ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 ) | |
7 | eqid | ⊢ ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 ) | |
8 | 1 7 4 | op01dm | ⊢ ( 𝐾 ∈ OP → ( 𝐵 ∈ dom ( lub ‘ 𝐾 ) ∧ 𝐵 ∈ dom ( glb ‘ 𝐾 ) ) ) |
9 | 8 | simprd | ⊢ ( 𝐾 ∈ OP → 𝐵 ∈ dom ( glb ‘ 𝐾 ) ) |
10 | 9 | adantr | ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → 𝐵 ∈ dom ( glb ‘ 𝐾 ) ) |
11 | 1 4 2 3 5 6 10 | p0le | ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → 0 ≤ 𝑋 ) |