Theorem opnlen0

Description: An element not less than another is nonzero. TODO: Look for uses of necon3bd and op0le to see if this is useful elsewhere. (Contributed by NM, 5-May-2013)

	Ref	Expression
Hypotheses	op0le.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	op0le.l	⊢ ≤ = ( le ‘ 𝐾 )
	op0le.z	⊢ 0 = ( 0. ‘ 𝐾 )
Assertion	opnlen0	⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑋 ≤ 𝑌 ) → 𝑋 ≠ 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	3adant2	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 0 ≤ 𝑌 )
6		breq1	⊢ ( 𝑋 = 0 → ( 𝑋 ≤ 𝑌 ↔ 0 ≤ 𝑌 ) )
7	5 6	syl5ibrcom	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 = 0 → 𝑋 ≤ 𝑌 ) )
8	7	necon3bd	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ¬ 𝑋 ≤ 𝑌 → 𝑋 ≠ 0 ) )
9	8	imp	⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ 𝑋 ≤ 𝑌 ) → 𝑋 ≠ 0 )