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

Metamath Proof Explorer

Theorem op1le

Description: If the orthoposet unity 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 ⊢ B = Base K
ople1.l ⊢ ≤ ˙ = ≤ K
ople1.u ⊢ 1 ˙ = 1. ⁡ K
Assertion op1le ⊢ K ∈ OP ∧ X ∈ B → 1 ˙ ≤ ˙ X ↔ X = 1 ˙

Proof

Step Hyp Ref Expression
1 ople1.b ⊢ B = Base K
2 ople1.l ⊢ ≤ ˙ = ≤ K
3 ople1.u ⊢ 1 ˙ = 1. ⁡ K
4 1 2 3 ople1 ⊢ K ∈ OP ∧ X ∈ B → X ≤ ˙ 1 ˙
5 4 biantrurd ⊢ K ∈ OP ∧ X ∈ B → 1 ˙ ≤ ˙ X ↔ X ≤ ˙ 1 ˙ ∧ 1 ˙ ≤ ˙ X
6 opposet ⊢ K ∈ OP → K ∈ Poset
7 6 adantr ⊢ K ∈ OP ∧ X ∈ B → K ∈ Poset
8 simpr ⊢ K ∈ OP ∧ X ∈ B → X ∈ B
9 1 3 op1cl ⊢ K ∈ OP → 1 ˙ ∈ B
10 9 adantr ⊢ K ∈ OP ∧ X ∈ B → 1 ˙ ∈ B
11 1 2 posasymb ⊢ K ∈ Poset ∧ X ∈ B ∧ 1 ˙ ∈ B → X ≤ ˙ 1 ˙ ∧ 1 ˙ ≤ ˙ X ↔ X = 1 ˙
12 7 8 10 11 syl3anc ⊢ K ∈ OP ∧ X ∈ B → X ≤ ˙ 1 ˙ ∧ 1 ˙ ≤ ˙ X ↔ X = 1 ˙
13 5 12 bitrd ⊢ K ∈ OP ∧ X ∈ B → 1 ˙ ≤ ˙ X ↔ X = 1 ˙