Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  joinle Structured version   Unicode version

Theorem joinle 15770
 Description: A join is less than or equal to a third value iff each argument is less than or equal to the third value. (Contributed by NM, 16-Sep-2011.)
Hypotheses
Ref Expression
joinle.b
joinle.l
joinle.j
joinle.k
joinle.x
joinle.y
joinle.z
joinle.e
Assertion
Ref Expression
joinle

Proof of Theorem joinle
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 joinle.z . . 3
2 joinle.b . . . . 5
3 joinle.l . . . . 5
4 joinle.j . . . . 5
5 joinle.k . . . . 5
6 joinle.x . . . . 5
7 joinle.y . . . . 5
8 joinle.e . . . . 5
92, 3, 4, 5, 6, 7, 8joinlem 15767 . . . 4
109simprd 463 . . 3
11 breq2 4460 . . . . . 6
12 breq2 4460 . . . . . 6
1311, 12anbi12d 710 . . . . 5
14 breq2 4460 . . . . 5
1513, 14imbi12d 320 . . . 4
1615rspcva 3208 . . 3
171, 10, 16syl2anc 661 . 2
182, 3, 4, 5, 6, 7, 8lejoin1 15768 . . . 4
192, 4, 5, 6, 7, 8joincl 15762 . . . . 5
202, 3postr 15709 . . . . 5
215, 6, 19, 1, 20syl13anc 1230 . . . 4
2218, 21mpand 675 . . 3
232, 3, 4, 5, 6, 7, 8lejoin2 15769 . . . 4
242, 3postr 15709 . . . . 5
255, 7, 19, 1, 24syl13anc 1230 . . . 4
2623, 25mpand 675 . . 3