Theorem ople0

Description: An element less than or equal to zero equals zero. ( chle0 analog.) (Contributed by NM, 21-Oct-2011)

	Ref	Expression
Hypotheses	op0le.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	op0le.l	⊢ ≤ = ( le ‘ 𝐾 )
	op0le.z	⊢ 0 = ( 0. ‘ 𝐾 )
Assertion	ople0	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ≤ 0 ↔ 𝑋 = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		op0le.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		op0le.l	⊢ ≤ = ( le ‘ 𝐾 )
3		op0le.z	⊢ 0 = ( 0. ‘ 𝐾 )
4	1 2 3	op0le	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → 0 ≤ 𝑋 )
5	4	biantrud	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ≤ 0 ↔ ( 𝑋 ≤ 0 ∧ 0 ≤ 𝑋 ) ) )
6		opposet	⊢ ( 𝐾 ∈ OP → 𝐾 ∈ Poset )
7	6	adantr	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → 𝐾 ∈ Poset )
8		simpr	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
9	1 3	op0cl	⊢ ( 𝐾 ∈ OP → 0 ∈ 𝐵 )
10	9	adantr	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → 0 ∈ 𝐵 )
11	1 2	posasymb	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 0 ∈ 𝐵 ) → ( ( 𝑋 ≤ 0 ∧ 0 ≤ 𝑋 ) ↔ 𝑋 = 0 ) )
12	7 8 10 11	syl3anc	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑋 ≤ 0 ∧ 0 ≤ 𝑋 ) ↔ 𝑋 = 0 ) )
13	5 12	bitrd	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ≤ 0 ↔ 𝑋 = 0 ) )