Metamath Proof Explorer


Theorem op1le

Description: If the orthoposet unit is less than or equal to an element, the element equals the unit. ( chle0 analog.) (Contributed by NM, 5-Dec-2011)

Ref Expression
Hypotheses ople1.b 𝐵 = ( Base ‘ 𝐾 )
ople1.l = ( le ‘ 𝐾 )
ople1.u 1 = ( 1. ‘ 𝐾 )
Assertion op1le ( ( 𝐾 ∈ OP ∧ 𝑋𝐵 ) → ( 1 𝑋𝑋 = 1 ) )

Proof

Step Hyp Ref Expression
1 ople1.b 𝐵 = ( Base ‘ 𝐾 )
2 ople1.l = ( le ‘ 𝐾 )
3 ople1.u 1 = ( 1. ‘ 𝐾 )
4 1 2 3 ople1 ( ( 𝐾 ∈ OP ∧ 𝑋𝐵 ) → 𝑋 1 )
5 4 biantrurd ( ( 𝐾 ∈ OP ∧ 𝑋𝐵 ) → ( 1 𝑋 ↔ ( 𝑋 11 𝑋 ) ) )
6 opposet ( 𝐾 ∈ OP → 𝐾 ∈ Poset )
7 6 adantr ( ( 𝐾 ∈ OP ∧ 𝑋𝐵 ) → 𝐾 ∈ Poset )
8 simpr ( ( 𝐾 ∈ OP ∧ 𝑋𝐵 ) → 𝑋𝐵 )
9 1 3 op1cl ( 𝐾 ∈ OP → 1𝐵 )
10 9 adantr ( ( 𝐾 ∈ OP ∧ 𝑋𝐵 ) → 1𝐵 )
11 1 2 posasymb ( ( 𝐾 ∈ Poset ∧ 𝑋𝐵1𝐵 ) → ( ( 𝑋 11 𝑋 ) ↔ 𝑋 = 1 ) )
12 7 8 10 11 syl3anc ( ( 𝐾 ∈ OP ∧ 𝑋𝐵 ) → ( ( 𝑋 11 𝑋 ) ↔ 𝑋 = 1 ) )
13 5 12 bitrd ( ( 𝐾 ∈ OP ∧ 𝑋𝐵 ) → ( 1 𝑋𝑋 = 1 ) )