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 ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝑌 ↔ ( 𝑋 < 𝑌𝑋 = 𝑌 ) ) )