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

Metamath Proof Explorer

Theorem pleval2

Description: "Less than or equal to" in terms of "less than". ( sspss analog.) (Contributed by NM, 17-Oct-2011) (Revised by Mario Carneiro, 8-Feb-2015)

		Ref	Expression
	Hypotheses	pleval2.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
		pleval2.l	⊢ ≤ = ( le ‘ 𝐾 )
		pleval2.s	⊢ < = ( lt ‘ 𝐾 )
	Assertion	pleval2	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 ↔ ( 𝑋 < 𝑌 ∨ 𝑋 = 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pleval2.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		pleval2.l	⊢ ≤ = ( le ‘ 𝐾 )
3		pleval2.s	⊢ < = ( lt ‘ 𝐾 )
4	1 2 3	pleval2i	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 → ( 𝑋 < 𝑌 ∨ 𝑋 = 𝑌 ) ) )
5	4	3adant1	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 → ( 𝑋 < 𝑌 ∨ 𝑋 = 𝑌 ) ) )
6	2 3	pltle	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 → 𝑋 ≤ 𝑌 ) )
7	1 2	posref	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ≤ 𝑋 )
8	7	3adant3	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ≤ 𝑋 )
9		breq2	⊢ ( 𝑋 = 𝑌 → ( 𝑋 ≤ 𝑋 ↔ 𝑋 ≤ 𝑌 ) )
10	8 9	syl5ibcom	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 = 𝑌 → 𝑋 ≤ 𝑌 ) )
11	6 10	jaod	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 < 𝑌 ∨ 𝑋 = 𝑌 ) → 𝑋 ≤ 𝑌 ) )
12	5 11	impbid	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 ↔ ( 𝑋 < 𝑌 ∨ 𝑋 = 𝑌 ) ) )