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

Theorem joinle 14455
 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
joinval2.b
joinval2.l
joinval2.j
Assertion
Ref Expression
joinle

Proof of Theorem joinle
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 joinval2.b . . . . . . . . . 10
2 joinval2.l . . . . . . . . . 10
3 joinval2.j . . . . . . . . . 10
41, 2, 3joinlem 14452 . . . . . . . . 9
54simprd 451 . . . . . . . 8
6 breq2 4219 . . . . . . . . . . 11
7 breq2 4219 . . . . . . . . . . 11
86, 7anbi12d 693 . . . . . . . . . 10
9 breq2 4219 . . . . . . . . . 10
108, 9imbi12d 313 . . . . . . . . 9
1110rspccv 3051 . . . . . . . 8
125, 11syl 16 . . . . . . 7
1312ex 425 . . . . . 6
1413com23 75 . . . . 5
15143exp 1153 . . . 4
16153impd 1168 . . 3
17163imp 1148 . 2
181, 2, 3lejoin1 14453 . . . . . . 7
1918ex 425 . . . . . 6
20193adant3r3 1165 . . . . 5
21203impia 1151 . . . 4
221, 2postr 14415 . . . . . . . . 9
23223exp2 1172 . . . . . . . 8
2423com34 80 . . . . . . 7
2524imp32 424 . . . . . 6
26253adantr2 1118 . . . . 5
27263impia 1151 . . . 4
2821, 27mpand 658 . . 3
291, 2, 3lejoin2 14454 . . . . . . 7
3029ex 425 . . . . . 6
31303adant3r3 1165 . . . . 5
32313impia 1151 . . . 4
331, 2postr 14415 . . . . . . . . 9
34333exp2 1172 . . . . . . . 8
3534com34 80 . . . . . . 7
36353imp 1148 . . . . . 6
37363adant3r1 1163 . . . . 5
38373impia 1151 . . . 4
3932, 38mpand 658 . . 3