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 B=BaseK
pleval2.l ˙=K
pleval2.s <˙=<K
Assertion pleval2 KPosetXBYBX˙YX<˙YX=Y

Proof

Step Hyp Ref Expression
1 pleval2.b B=BaseK
2 pleval2.l ˙=K
3 pleval2.s <˙=<K
4 1 2 3 pleval2i XBYBX˙YX<˙YX=Y
5 4 3adant1 KPosetXBYBX˙YX<˙YX=Y
6 2 3 pltle KPosetXBYBX<˙YX˙Y
7 1 2 posref KPosetXBX˙X
8 7 3adant3 KPosetXBYBX˙X
9 breq2 X=YX˙XX˙Y
10 8 9 syl5ibcom KPosetXBYBX=YX˙Y
11 6 10 jaod KPosetXBYBX<˙YX=YX˙Y
12 5 11 impbid KPosetXBYBX˙YX<˙YX=Y